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

Metamath Proof Explorer

Theorem r3al

Description: Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995) (Proof shortened by Wolf Lammen, 30-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 r2al 
 |-  ( A. x e. A A. y e. B A. z e. C ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> A. z e. C ph ) )
2 19.21v 
 |-  ( A. z ( ( x e. A /\ y e. B ) -> ( z e. C -> ph ) ) <-> ( ( x e. A /\ y e. B ) -> A. z ( z e. C -> ph ) ) )
3 df-3an 
 |-  ( ( x e. A /\ y e. B /\ z e. C ) <-> ( ( x e. A /\ y e. B ) /\ z e. C ) )
4 3 imbi1i 
 |-  ( ( ( x e. A /\ y e. B /\ z e. C ) -> ph ) <-> ( ( ( x e. A /\ y e. B ) /\ z e. C ) -> ph ) )
5 impexp 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ z e. C ) -> ph ) <-> ( ( x e. A /\ y e. B ) -> ( z e. C -> ph ) ) )
6 4 5 bitri 
 |-  ( ( ( x e. A /\ y e. B /\ z e. C ) -> ph ) <-> ( ( x e. A /\ y e. B ) -> ( z e. C -> ph ) ) )
7 6 albii 
 |-  ( A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ph ) <-> A. z ( ( x e. A /\ y e. B ) -> ( z e. C -> ph ) ) )
8 df-ral 
 |-  ( A. z e. C ph <-> A. z ( z e. C -> ph ) )
9 8 imbi2i 
 |-  ( ( ( x e. A /\ y e. B ) -> A. z e. C ph ) <-> ( ( x e. A /\ y e. B ) -> A. z ( z e. C -> ph ) ) )
10 2 7 9 3bitr4ri 
 |-  ( ( ( x e. A /\ y e. B ) -> A. z e. C ph ) <-> A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ph ) )
11 10 2albii 
 |-  ( A. x A. y ( ( x e. A /\ y e. B ) -> A. z e. C ph ) <-> A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ph ) )
12 1 11 bitri 
 |-  ( A. x e. A A. y e. B A. z e. C ph <-> A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ph ) )