This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 19.32

Description: Theorem 19.32 of Margaris p. 90. See 19.32v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993) (Revised by Mario Carneiro, 24-Sep-2016)

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

Proof

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