 Formulas in the classical equivalential calculus are written using sentential variables and a two-place function symbol, e, for equivalence. The calculus has two rules of inference, detachment (modus ponens) and substitution; the rules can be combined into the single rule of condensed detachment: Obtain tθ from e(s,t) and r where sθ = rθ with mgu θ. The calculus can be axiomatized with the formulas: 