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

Metamath Proof Explorer

Theorem eeor

Description: Distribute existential quantifiers. (Contributed by NM, 8-Aug-1994) Avoid ax-10 . (Revised by GG, 21-Nov-2024)

Ref Expression
Hypotheses eeor.1 
|- F/ y ph
eeor.2 
|- F/ x ps
Assertion eeor 
|- ( E. x E. y ( ph \/ ps ) <-> ( E. x ph \/ E. y ps ) )

Proof

Step Hyp Ref Expression
1 eeor.1 
 |-  F/ y ph
2 eeor.2 
 |-  F/ x ps
3 19.43 
 |-  ( E. y ( ph \/ ps ) <-> ( E. y ph \/ E. y ps ) )
4 3 exbii 
 |-  ( E. x E. y ( ph \/ ps ) <-> E. x ( E. y ph \/ E. y ps ) )
5 19.43 
 |-  ( E. x ( E. y ph \/ E. y ps ) <-> ( E. x E. y ph \/ E. x E. y ps ) )
6 1 19.9 
 |-  ( E. y ph <-> ph )
7 6 exbii 
 |-  ( E. x E. y ph <-> E. x ph )
8 excom 
 |-  ( E. x E. y ps <-> E. y E. x ps )
9 2 19.9 
 |-  ( E. x ps <-> ps )
10 9 exbii 
 |-  ( E. y E. x ps <-> E. y ps )
11 8 10 bitri 
 |-  ( E. x E. y ps <-> E. y ps )
12 7 11 orbi12i 
 |-  ( ( E. x E. y ph \/ E. x E. y ps ) <-> ( E. x ph \/ E. y ps ) )
13 5 12 bitri 
 |-  ( E. x ( E. y ph \/ E. y ps ) <-> ( E. x ph \/ E. y ps ) )
14 4 13 bitri 
 |-  ( E. x E. y ( ph \/ ps ) <-> ( E. x ph \/ E. y ps ) )