Theorem vtocl2d

Description: Implicit substitution of two classes for two setvar variables. (Contributed by Thierry Arnoux, 25-Aug-2020) (Revised by BTernaryTau, 19-Oct-2023)

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

Proof

Step	Hyp	Ref	Expression
1		vtocl2d.a	$$⊢\phi \to A\in V$$
2		vtocl2d.b	$$⊢\phi \to B\in W$$
3		vtocl2d.1	$$⊢\left(x=A\wedge y=B\right)\to \left(\psi \leftrightarrow \chi \right)$$
4		vtocl2d.3	$$⊢\phi \to \psi$$
5	4	adantr	$$⊢\left(\phi \wedge y=B\right)\to \psi$$
6	3	adantll	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to \left(\psi \leftrightarrow \chi \right)$$
7	6	pm5.74da	$$⊢\left(\phi \wedge x=A\right)\to \left(\left(y=B\to \psi \right)\leftrightarrow \left(y=B\to \chi \right)\right)$$
8	4	a1d	$$⊢\phi \to \left(y=B\to \psi \right)$$
9	1 7 8	vtocld	$$⊢\phi \to \left(y=B\to \chi \right)$$
10	9	imp	$$⊢\left(\phi \wedge y=B\right)\to \chi$$
11	5 10	2thd	$$⊢\left(\phi \wedge y=B\right)\to \left(\psi \leftrightarrow \chi \right)$$
12	2 11 4	vtocld	$$⊢\phi \to \chi$$