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 Gino Giotto, 3-Oct-2024)

		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		eleq1	$⊢ x = A \to (x \in D \leftrightarrow A \in D)$
6	5	3anbi1d	$⊢ x = A \to ((x \in D \land y \in R \land z \in S) \leftrightarrow (A \in D \land y \in R \land z \in S))$
7	6 1	imbi12d	$⊢ x = A \to (((x \in D \land y \in R \land z \in S) \to φ) \leftrightarrow ((A \in D \land y \in R \land z \in S) \to ψ))$
8		eleq1	$⊢ y = B \to (y \in R \leftrightarrow B \in R)$
9	8	3anbi2d	$⊢ y = B \to ((A \in D \land y \in R \land z \in S) \leftrightarrow (A \in D \land B \in R \land z \in S))$
10	9 2	imbi12d	$⊢ y = B \to (((A \in D \land y \in R \land z \in S) \to ψ) \leftrightarrow ((A \in D \land B \in R \land z \in S) \to χ))$
11		eleq1	$⊢ z = C \to (z \in S \leftrightarrow C \in S)$
12	11	3anbi3d	$⊢ z = C \to ((A \in D \land B \in R \land z \in S) \leftrightarrow (A \in D \land B \in R \land C \in S))$
13	12 3	imbi12d	$⊢ z = C \to (((A \in D \land B \in R \land z \in S) \to χ) \leftrightarrow ((A \in D \land B \in R \land C \in S) \to θ))$
14	7 10 13 4	vtocl3g	$⊢ (A \in D \land B \in R \land C \in S) \to ((A \in D \land B \in R \land C \in S) \to θ)$
15	14	pm2.43i	$⊢ (A \in D \land B \in R \land C \in S) \to θ$