Metamath Proof Explorer

Theorem r3ex

Description: Triple existential quantification. (Contributed by AV, 21-Jul-2025)

Ref Expression
Assertion r3ex 
|- ( E. x e. A E. y e. B E. z e. C ph <-> E. x E. y E. z ( ( x e. A /\ y e. B /\ z e. C ) /\ ph ) )

Proof

Step Hyp Ref Expression
1 r2ex 
 |-  ( E. x e. A E. y e. B E. z e. C ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ E. z e. C ph ) )
2 df-rex 
 |-  ( E. z e. C ph <-> E. z ( z e. C /\ ph ) )
3 2 anbi2i 
 |-  ( ( ( x e. A /\ y e. B ) /\ E. z e. C ph ) <-> ( ( x e. A /\ y e. B ) /\ E. z ( z e. C /\ ph ) ) )
4 19.42v 
 |-  ( E. z ( ( x e. A /\ y e. B ) /\ ( z e. C /\ ph ) ) <-> ( ( x e. A /\ y e. B ) /\ E. z ( z e. C /\ ph ) ) )
5 anass 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ z e. C ) /\ ph ) <-> ( ( x e. A /\ y e. B ) /\ ( z e. C /\ ph ) ) )
6 5 bicomi 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ ph ) ) <-> ( ( ( x e. A /\ y e. B ) /\ z e. C ) /\ ph ) )
7 df-3an 
 |-  ( ( x e. A /\ y e. B /\ z e. C ) <-> ( ( x e. A /\ y e. B ) /\ z e. C ) )
8 7 bicomi 
 |-  ( ( ( x e. A /\ y e. B ) /\ z e. C ) <-> ( x e. A /\ y e. B /\ z e. C ) )
9 6 8 bianbi 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ ph ) ) <-> ( ( x e. A /\ y e. B /\ z e. C ) /\ ph ) )
10 9 exbii 
 |-  ( E. z ( ( x e. A /\ y e. B ) /\ ( z e. C /\ ph ) ) <-> E. z ( ( x e. A /\ y e. B /\ z e. C ) /\ ph ) )
11 3 4 10 3bitr2i 
 |-  ( ( ( x e. A /\ y e. B ) /\ E. z e. C ph ) <-> E. z ( ( x e. A /\ y e. B /\ z e. C ) /\ ph ) )
12 11 2exbii 
 |-  ( E. x E. y ( ( x e. A /\ y e. B ) /\ E. z e. C ph ) <-> E. x E. y E. z ( ( x e. A /\ y e. B /\ z e. C ) /\ ph ) )
13 1 12 bitri 
 |-  ( E. x e. A E. y e. B E. z e. C ph <-> E. x E. y E. z ( ( x e. A /\ y e. B /\ z e. C ) /\ ph ) )