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 )