Theorem 19.31

Description: Theorem 19.31 of Margaris p. 90. See 19.31v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993)

	Ref	Expression
Hypothesis	19.31.1	|- F/ x ps
Assertion	19.31	|- ( A. x ( ph \/ ps ) <-> ( A. x ph \/ ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.31.1	|- F/ x ps
2	1	19.32	|- ( A. x ( ps \/ ph ) <-> ( ps \/ A. x ph ) )
3		orcom	|- ( ( ph \/ ps ) <-> ( ps \/ ph ) )
4	3	albii	|- ( A. x ( ph \/ ps ) <-> A. x ( ps \/ ph ) )
5		orcom	|- ( ( A. x ph \/ ps ) <-> ( ps \/ A. x ph ) )
6	2 4 5	3bitr4i	|- ( A. x ( ph \/ ps ) <-> ( A. x ph \/ ps ) )