Theorem vtocl3gaOLDOLD

Description: Obsolete version of vtocl3ga as of 3-Oct-2024. (Contributed by NM, 20-Aug-1995) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vtocl3gaOLDOLD.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	vtocl3gaOLDOLD.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
	vtocl3gaOLDOLD.3	$$⊢z=C\to \left(\chi \leftrightarrow \theta \right)$$
	vtocl3gaOLDOLD.4	$$⊢\left(x\in D\wedge y\in R\wedge z\in S\right)\to \phi$$
Assertion	vtocl3gaOLDOLD	$$⊢\left(A\in D\wedge B\in R\wedge C\in S\right)\to \theta$$

Proof

Step	Hyp	Ref	Expression
1		vtocl3gaOLDOLD.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		vtocl3gaOLDOLD.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
3		vtocl3gaOLDOLD.3	$$⊢z=C\to \left(\chi \leftrightarrow \theta \right)$$
4		vtocl3gaOLDOLD.4	$$⊢\left(x\in D\wedge y\in R\wedge z\in S\right)\to \phi$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}zA$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}zB$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}zC$$
11		nfv	$$⊢Ⅎx\psi$$
12		nfv	$$⊢Ⅎy\chi$$
13		nfv	$$⊢Ⅎz\theta$$
14	5 6 7 8 9 10 11 12 13 1 2 3 4	vtocl3gaf	$$⊢\left(A\in D\wedge B\in R\wedge C\in S\right)\to \theta$$