Theorem 3gencl 2715

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

Hypotheses

Ref	Expression
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

Ref	Expression
3gencl	|- ( ( D e. S /\ F e. S /\ G e. S ) -> th )

Distinct variable groups:   x, y, z   y, D, z   z, F   x, R, y   y, S, z   ps, x   ch, y   th, z

Allowed substitution hints:   ph( x, y, z)   ps( y, z)   ch( x, z)   th( x, y)   A( x, y, z)   B( x, y, z)   C( x, y, z)   D( x)   R( z)   S( x)   F( x, y)   G( x, y, z)

Proof of Theorem 3gencl

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 962   = wceq 1331   E.wex 1468   e. wcel 1480   E.wrex 2415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie2 1470  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-3an 964  df-rex 2420

This theorem is referenced by:  axpre-ltwlin  7684  axpre-lttrn  7685  axpre-ltadd  7687  axpre-mulext  7689