Prove:

(== => =) ,

under the assumption:

(= => Fa = => =) .

For proving (== => =) we take all variables arbitrary but fixed and prove:

(1) .

We prove (1) by the deduction rule.

We assume

(2)

and show

(3) .

The conjunction (2) splits into (4) , (5) .

From (5) , by (= => Fa = => =) , we obtain:

(7) .

From (4) , by (= => Fa = => =) , we obtain:

(6) .

For proving (3) , by (6) , it suffices to prove

(9) .

Formula (9) is true because it is identical to (5) .

---

Converted by Mathematica      February 11, 2000