Theorem vtocl3ga

Description: Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995)

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

Proof

Step	Hyp	Ref	Expression
1		vtocl3ga.1	|- ( x = A -> ( ph <-> ps ) )
2		vtocl3ga.2	|- ( y = B -> ( ps <-> ch ) )
3		vtocl3ga.3	|- ( z = C -> ( ch <-> th ) )
4		vtocl3ga.4	|- ( ( x e. D /\ y e. R /\ z e. S ) -> ph )
5		nfcv	|- F/_ x A
6		nfcv	|- F/_ y A
7		nfcv	|- F/_ z A
8		nfcv	|- F/_ y B
9		nfcv	|- F/_ z B
10		nfcv	|- F/_ z C
11		nfv	|- F/ x ps
12		nfv	|- F/ y ch
13		nfv	|- F/ z th
14	5 6 7 8 9 10 11 12 13 1 2 3 4	vtocl3gaf	|- ( ( A e. D /\ B e. R /\ C e. S ) -> th )