vtocl4g

Description: Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019)

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

Step	Hyp	Ref	Expression
1		vtocl4g.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		vtocl4g.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
3		vtocl4g.3	$⊢ z = C \to (χ \leftrightarrow ρ)$
4		vtocl4g.4	$⊢ w = D \to (ρ \leftrightarrow θ)$
5		vtocl4g.5	$⊢ φ$
6	3	imbi2d	$⊢ z = C \to (((A \in Q \land B \in R) \to χ) \leftrightarrow ((A \in Q \land B \in R) \to ρ))$
7	4	imbi2d	$⊢ w = D \to (((A \in Q \land B \in R) \to ρ) \leftrightarrow ((A \in Q \land B \in R) \to θ))$
8	1 2 5	vtocl2g	$⊢ (A \in Q \land B \in R) \to χ$
9	6 7 8	vtocl2g	$⊢ (C \in S \land D \in T) \to ((A \in Q \land B \in R) \to θ)$
10	9	impcom	$⊢ ((A \in Q \land B \in R) \land (C \in S \land D \in T)) \to θ$

Metamath Proof Explorer