This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtocl4ga

Description: Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019) (Proof shortened by Wolf Lammen, 31-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		vtocl4ga.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		vtocl4ga.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
3		vtocl4ga.3	$⊢ z = C \to (χ \leftrightarrow ρ)$
4		vtocl4ga.4	$⊢ w = D \to (ρ \leftrightarrow θ)$
5		vtocl4ga.5	$⊢ ((x \in Q \land y \in R) \land (z \in S \land w \in T)) \to φ$
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	imbi2d	$⊢ x = A \to (((z \in S \land w \in T) \to φ) \leftrightarrow ((z \in S \land w \in T) \to ψ))$
9	2	imbi2d	$⊢ y = B \to (((z \in S \land w \in T) \to ψ) \leftrightarrow ((z \in S \land w \in T) \to χ))$
10	5	ex	$⊢ (x \in Q \land y \in R) \to ((z \in S \land w \in T) \to φ)$
11	8 9 10	vtocl2ga	$⊢ (A \in Q \land B \in R) \to ((z \in S \land w \in T) \to χ)$
12	11	com12	$⊢ (z \in S \land w \in T) \to ((A \in Q \land B \in R) \to χ)$
13	6 7 12	vtocl2ga	$⊢ (C \in S \land D \in T) \to ((A \in Q \land B \in R) \to θ)$
14	13	impcom	$⊢ ((A \in Q \land B \in R) \land (C \in S \land D \in T)) \to θ$