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

Metamath Proof Explorer

Theorem 3gencl

Description: Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996)

Ref Expression
Hypotheses 3gencl.1 
|- ( D e. S <-> E. x e. R A = D )
3gencl.2 
|- ( F e. S <-> E. y e. R B = F )
3gencl.3 
|- ( G e. S <-> E. z e. R C = G )
3gencl.4 
|- ( A = D -> ( ph <-> ps ) )
3gencl.5 
|- ( B = F -> ( ps <-> ch ) )
3gencl.6 
|- ( C = G -> ( ch <-> th ) )
3gencl.7 
|- ( ( x e. R /\ y e. R /\ z e. R ) -> ph )
Assertion 3gencl 
|- ( ( D e. S /\ F e. S /\ G e. S ) -> th )

Proof

Step Hyp Ref Expression
1 3gencl.1 
 |-  ( D e. S <-> E. x e. R A = D )
2 3gencl.2 
 |-  ( F e. S <-> E. y e. R B = F )
3 3gencl.3 
 |-  ( G e. S <-> E. z e. R C = G )
4 3gencl.4 
 |-  ( A = D -> ( ph <-> ps ) )
5 3gencl.5 
 |-  ( B = F -> ( ps <-> ch ) )
6 3gencl.6 
 |-  ( C = G -> ( ch <-> th ) )
7 3gencl.7 
 |-  ( ( x e. R /\ y e. R /\ z e. R ) -> ph )
8 df-rex 
 |-  ( E. z e. R C = G <-> E. z ( z e. R /\ C = G ) )
9 3 8 bitri 
 |-  ( G e. S <-> E. z ( z e. R /\ C = G ) )
10 6 imbi2d 
 |-  ( C = G -> ( ( ( D e. S /\ F e. S ) -> ch ) <-> ( ( D e. S /\ F e. S ) -> th ) ) )
11 4 imbi2d 
 |-  ( A = D -> ( ( z e. R -> ph ) <-> ( z e. R -> ps ) ) )
12 5 imbi2d 
 |-  ( B = F -> ( ( z e. R -> ps ) <-> ( z e. R -> ch ) ) )
13 7 3expia 
 |-  ( ( x e. R /\ y e. R ) -> ( z e. R -> ph ) )
14 1 2 11 12 13 2gencl 
 |-  ( ( D e. S /\ F e. S ) -> ( z e. R -> ch ) )
15 14 com12 
 |-  ( z e. R -> ( ( D e. S /\ F e. S ) -> ch ) )
16 9 10 15 gencl 
 |-  ( G e. S -> ( ( D e. S /\ F e. S ) -> th ) )
17 16 com12 
 |-  ( ( D e. S /\ F e. S ) -> ( G e. S -> th ) )
18 17 3impia 
 |-  ( ( D e. S /\ F e. S /\ G e. S ) -> th )