Theorem 3gencl 3237

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 2918	. . . . 5 |- ( E. z e. R C = G <-> E. z ( z e. R /\ C = G ) )
3	1, 2	bitri 264	. . . 4 |- ( G e. S <-> E. z ( z e. R /\ C = G ) )
4		3gencl.6	. . . . 5 |- ( C = G -> ( ch <-> th ) )
5	4	imbi2d 330	. . . 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 330	. . . . . 6 |- ( A = D -> ( ( z e. R -> ph ) <-> ( z e. R -> ps ) ) )
10		3gencl.5	. . . . . . 7 |- ( B = F -> ( ps <-> ch ) )
11	10	imbi2d 330	. . . . . 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 1267	. . . . . 6 |- ( ( x e. R /\ y e. R ) -> ( z e. R -> ph ) )
14	6, 7, 9, 11, 13	2gencl 3236	. . . . 5 |- ( ( D e. S /\ F e. S ) -> ( z e. R -> ch ) )
15	14	com12 32	. . . 4 |- ( z e. R -> ( ( D e. S /\ F e. S ) -> ch ) )
16	3, 5, 15	gencl 3235	. . 3 |- ( G e. S -> ( ( D e. S /\ F e. S ) -> th ) )
17	16	com12 32	. 2 |- ( ( D e. S /\ F e. S ) -> ( G e. S -> th ) )
18	17	3impia 1261	1 |- ( ( D e. S /\ F e. S /\ G e. S ) -> th )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039  df-ex 1705  df-rex 2918

This theorem is referenced by:  axpre-lttrn  9987  axpre-ltadd  9988