Metamath Proof Explorer

Theorem vtocl3ga

Description: Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995) Reduce axiom usage. (Revised by GG, 3-Oct-2024) (Proof shortened by Wolf Lammen, 31-May-2025)

		Ref	Expression
	Hypotheses	vtocl3ga.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
		vtocl3ga.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
		vtocl3ga.3	$⊢ z = C \to (χ \leftrightarrow θ)$
		vtocl3ga.4	$⊢ (x \in D \land y \in R \land z \in S) \to φ$
	Assertion	vtocl3ga	$⊢ (A \in D \land B \in R \land C \in S) \to θ$

Proof

Step	Hyp	Ref	Expression
1		vtocl3ga.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		vtocl3ga.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
3		vtocl3ga.3	$⊢ z = C \to (χ \leftrightarrow θ)$
4		vtocl3ga.4	$⊢ (x \in D \land y \in R \land z \in S) \to φ$
5	3	imbi2d	$⊢ z = C \to (((A \in D \land B \in R) \to χ) \leftrightarrow ((A \in D \land B \in R) \to θ))$
6	1	imbi2d	$⊢ x = A \to ((z \in S \to φ) \leftrightarrow (z \in S \to ψ))$
7	2	imbi2d	$⊢ y = B \to ((z \in S \to ψ) \leftrightarrow (z \in S \to χ))$
8	4	3expia	$⊢ (x \in D \land y \in R) \to (z \in S \to φ)$
9	6 7 8	vtocl2ga	$⊢ (A \in D \land B \in R) \to (z \in S \to χ)$
10	9	com12	$⊢ z \in S \to ((A \in D \land B \in R) \to χ)$
11	5 10	vtoclga	$⊢ C \in S \to ((A \in D \land B \in R) \to θ)$
12	11	impcom	$⊢ ((A \in D \land B \in R) \land C \in S) \to θ$
13	12	3impa	$⊢ (A \in D \land B \in R \land C \in S) \to θ$