Theorem vtocl3ga 2924

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

Hypotheses

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

Ref	Expression
vtocl3ga	|- ((A e. D /\ B e. R /\ C e. S) -> th)

Distinct variable groups:   x,y,z,A   y,B,z   z,C   x,D,y,z   x,R,y,z   x,S,y,z   ps,x   ch,y   th,z

Allowed substitution hints:   ph(x,y,z)   ps(y,z)   ch(x,z)   th(x,y)   B(x)   C(x,y)

Proof of Theorem vtocl3ga

Step	Hyp	Ref	Expression
1		nfcv 2489	. 2 |- F/_xA
2		nfcv 2489	. 2 |- F/_yA
3		nfcv 2489	. 2 |- F/_zA
4		nfcv 2489	. 2 |- F/_yB
5		nfcv 2489	. 2 |- F/_zB
6		nfcv 2489	. 2 |- F/_zC
7		nfv 1619	. 2 |- F/xps
8		nfv 1619	. 2 |- F/ych
9		nfv 1619	. 2 |- F/zth
10		vtocl3ga.1	. 2 |- (x = A -> (ph <-> ps))
11		vtocl3ga.2	. 2 |- (y = B -> (ps <-> ch))
12		vtocl3ga.3	. 2 |- (z = C -> (ch <-> th))
13		vtocl3ga.4	. 2 |- ((x e. D /\ y e. R /\ z e. S) -> ph)
14	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	vtocl3gaf 2923	1 |- ((A e. D /\ B e. R /\ C e. S) -> th)

Syntax hints:   -> wi 4   <-> wb 176   /\ w3a 934   = wceq 1642   e. wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861

This theorem is referenced by:  preq12bg  4128