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

Metamath Proof Explorer

Theorem 19.43OLD

Description: Obsolete proof of 19.43 . Do not delete as it is referenced on the mmrecent.html page and in conventions-labels . (Contributed by NM, 5-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 19.43OLD 
|- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) )

Proof

Step Hyp Ref Expression
1 ioran 
 |-  ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )
2 1 albii 
 |-  ( A. x -. ( ph \/ ps ) <-> A. x ( -. ph /\ -. ps ) )
3 19.26 
 |-  ( A. x ( -. ph /\ -. ps ) <-> ( A. x -. ph /\ A. x -. ps ) )
4 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
5 alnex 
 |-  ( A. x -. ps <-> -. E. x ps )
6 4 5 anbi12i 
 |-  ( ( A. x -. ph /\ A. x -. ps ) <-> ( -. E. x ph /\ -. E. x ps ) )
7 2 3 6 3bitri 
 |-  ( A. x -. ( ph \/ ps ) <-> ( -. E. x ph /\ -. E. x ps ) )
8 7 notbii 
 |-  ( -. A. x -. ( ph \/ ps ) <-> -. ( -. E. x ph /\ -. E. x ps ) )
9 df-ex 
 |-  ( E. x ( ph \/ ps ) <-> -. A. x -. ( ph \/ ps ) )
10 oran 
 |-  ( ( E. x ph \/ E. x ps ) <-> -. ( -. E. x ph /\ -. E. x ps ) )
11 8 9 10 3bitr4i 
 |-  ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) )