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

Metamath Proof Explorer

Theorem vtocl3gaOLD

Description: Obsolete version of vtocl3ga as of 31-May-2025. (Contributed by NM, 20-Aug-1995) Reduce axiom usage. (Revised by GG, 3-Oct-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vtocl3ga.1 ⊢ x = A → φ ↔ ψ
vtocl3ga.2 ⊢ y = B → ψ ↔ χ
vtocl3ga.3 ⊢ z = C → χ ↔ θ
vtocl3ga.4 ⊢ x ∈ D ∧ y ∈ R ∧ z ∈ S → φ
Assertion vtocl3gaOLD ⊢ 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 eleq1 ⊢ x = A → x ∈ D ↔ A ∈ D
6 5 3anbi1d ⊢ x = A → x ∈ D ∧ y ∈ R ∧ z ∈ S ↔ A ∈ D ∧ y ∈ R ∧ z ∈ S
7 6 1 imbi12d ⊢ x = A → x ∈ D ∧ y ∈ R ∧ z ∈ S → φ ↔ A ∈ D ∧ y ∈ R ∧ z ∈ S → ψ
8 eleq1 ⊢ y = B → y ∈ R ↔ B ∈ R
9 8 3anbi2d ⊢ y = B → A ∈ D ∧ y ∈ R ∧ z ∈ S ↔ A ∈ D ∧ B ∈ R ∧ z ∈ S
10 9 2 imbi12d ⊢ y = B → A ∈ D ∧ y ∈ R ∧ z ∈ S → ψ ↔ A ∈ D ∧ B ∈ R ∧ z ∈ S → χ
11 eleq1 ⊢ z = C → z ∈ S ↔ C ∈ S
12 11 3anbi3d ⊢ z = C → A ∈ D ∧ B ∈ R ∧ z ∈ S ↔ A ∈ D ∧ B ∈ R ∧ C ∈ S
13 12 3 imbi12d ⊢ z = C → A ∈ D ∧ B ∈ R ∧ z ∈ S → χ ↔ A ∈ D ∧ B ∈ R ∧ C ∈ S → θ
14 7 10 13 4 vtocl3g ⊢ A ∈ D ∧ B ∈ R ∧ C ∈ S → A ∈ D ∧ B ∈ R ∧ C ∈ S → θ
15 14 pm2.43i ⊢ A ∈ D ∧ B ∈ R ∧ C ∈ S → θ