Theorem 19.32v

Description: Version of 19.32 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020)

	Ref	Expression
Assertion	19.32v	|- ( A. x ( ph \/ ps ) <-> ( ph \/ A. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.21v	|- ( A. x ( -. ph -> ps ) <-> ( -. ph -> A. x ps ) )
2		df-or	|- ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
3	2	albii	|- ( A. x ( ph \/ ps ) <-> A. x ( -. ph -> ps ) )
4		df-or	|- ( ( ph \/ A. x ps ) <-> ( -. ph -> A. x ps ) )
5	1 3 4	3bitr4i	|- ( A. x ( ph \/ ps ) <-> ( ph \/ A. x ps ) )