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

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 → φ ↔ ψ
vtocl3ga.2 ⊢ y = B → ψ ↔ χ
vtocl3ga.3 ⊢ z = C → χ ↔ θ
vtocl3ga.4 ⊢ x ∈ D ∧ y ∈ R ∧ z ∈ S → φ
Assertion vtocl3ga ⊢ A ∈ D ∧ B ∈ R ∧ C ∈ S → θ

Proof

Step Hyp Ref Expression
1 vtocl3ga.1 ⊢ x = A → φ ↔ ψ
2 vtocl3ga.2 ⊢ y = B → ψ ↔ χ
3 vtocl3ga.3 ⊢ z = C → χ ↔ θ
4 vtocl3ga.4 ⊢ x ∈ D ∧ y ∈ R ∧ z ∈ S → φ
5 3 imbi2d ⊢ z = C → A ∈ D ∧ B ∈ R → χ ↔ A ∈ D ∧ B ∈ R → θ
6 1 imbi2d ⊢ x = A → z ∈ S → φ ↔ z ∈ S → ψ
7 2 imbi2d ⊢ y = B → z ∈ S → ψ ↔ z ∈ S → χ
8 4 3expia ⊢ x ∈ D ∧ y ∈ R → z ∈ S → φ
9 6 7 8 vtocl2ga ⊢ A ∈ D ∧ B ∈ R → z ∈ S → χ
10 9 com12 ⊢ z ∈ S → A ∈ D ∧ B ∈ R → χ
11 5 10 vtoclga ⊢ C ∈ S → A ∈ D ∧ B ∈ R → θ
12 11 impcom ⊢ A ∈ D ∧ B ∈ R ∧ C ∈ S → θ
13 12 3impa ⊢ A ∈ D ∧ B ∈ R ∧ C ∈ S → θ