Theorem vtocl2dOLD

Description: Obsolete version of vtocl2d as of 19-Oct-2023. (Contributed by Thierry Arnoux, 25-Aug-2020) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	vtocl2dOLD.a	$$⊢\phi \to A\in V$$
	vtocl2dOLD.b	$$⊢\phi \to B\in W$$
	vtocl2dOLD.1	$$⊢\left(x=A\wedge y=B\right)\to \left(\psi \leftrightarrow \chi \right)$$
	vtocl2dOLD.3	$$⊢\phi \to \psi$$
Assertion	vtocl2dOLD	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		vtocl2dOLD.a	$$⊢\phi \to A\in V$$
2		vtocl2dOLD.b	$$⊢\phi \to B\in W$$
3		vtocl2dOLD.1	$$⊢\left(x=A\wedge y=B\right)\to \left(\psi \leftrightarrow \chi \right)$$
4		vtocl2dOLD.3	$$⊢\phi \to \psi$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
8		nfv	$$⊢Ⅎy\phi$$
9		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi$$
10	8 9	nfim	$$⊢Ⅎy\left(\phi \to \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \right)$$
11		nfv	$$⊢Ⅎx\left(\phi \to \chi \right)$$
12		sbceq1a	$$⊢y=B\to \left(\psi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \right)$$
13	12	imbi2d	$$⊢y=B\to \left(\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \right)\right)$$
14		sbceq1a	$$⊢x=A\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \right)$$
15		nfv	$$⊢Ⅎx\chi$$
16		nfv	$$⊢Ⅎy\chi$$
17		nfv	$$⊢ℲxB\in W$$
18	15 16 17 3	sbc2iegf	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
19	1 2 18	syl2anc	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
20	14 19	sylan9bb	$$⊢\left(x=A\wedge \phi \right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
21	20	pm5.74da	$$⊢x=A\to \left(\left(\phi \to \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\phi \to \chi \right)\right)$$
22	5 6 7 10 11 13 21 4	vtocl2gf	$$⊢\left(B\in W\wedge A\in V\right)\to \left(\phi \to \chi \right)$$
23	2 1 22	syl2anc	$$⊢\phi \to \left(\phi \to \chi \right)$$
24	23	pm2.43i	$$⊢\phi \to \chi$$