Metamath Proof Explorer

Theorem vtocl4ga

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

Ref Expression
Hypotheses vtocl4ga.1 ⊢ x = A → φ ↔ ψ
vtocl4ga.2 ⊢ y = B → ψ ↔ χ
vtocl4ga.3 ⊢ z = C → χ ↔ ρ
vtocl4ga.4 ⊢ w = D → ρ ↔ θ
vtocl4ga.5 ⊢ x ∈ Q ∧ y ∈ R ∧ z ∈ S ∧ w ∈ T → φ
Assertion vtocl4ga ⊢ A ∈ Q ∧ B ∈ R ∧ C ∈ S ∧ D ∈ T → θ

Proof

Step Hyp Ref Expression
1 vtocl4ga.1 ⊢ x = A → φ ↔ ψ
2 vtocl4ga.2 ⊢ y = B → ψ ↔ χ
3 vtocl4ga.3 ⊢ z = C → χ ↔ ρ
4 vtocl4ga.4 ⊢ w = D → ρ ↔ θ
5 vtocl4ga.5 ⊢ x ∈ Q ∧ y ∈ R ∧ z ∈ S ∧ w ∈ T → φ
6 eleq1 ⊢ x = A → x ∈ Q ↔ A ∈ Q
7 6 anbi1d ⊢ x = A → x ∈ Q ∧ y ∈ R ↔ A ∈ Q ∧ y ∈ R
8 7 anbi1d ⊢ x = A → x ∈ Q ∧ y ∈ R ∧ z ∈ S ∧ w ∈ T ↔ A ∈ Q ∧ y ∈ R ∧ z ∈ S ∧ w ∈ T
9 8 1 imbi12d ⊢ x = A → x ∈ Q ∧ y ∈ R ∧ z ∈ S ∧ w ∈ T → φ ↔ A ∈ Q ∧ y ∈ R ∧ z ∈ S ∧ w ∈ T → ψ
10 eleq1 ⊢ y = B → y ∈ R ↔ B ∈ R
11 10 anbi2d ⊢ y = B → A ∈ Q ∧ y ∈ R ↔ A ∈ Q ∧ B ∈ R
12 11 anbi1d ⊢ y = B → A ∈ Q ∧ y ∈ R ∧ z ∈ S ∧ w ∈ T ↔ A ∈ Q ∧ B ∈ R ∧ z ∈ S ∧ w ∈ T
13 12 2 imbi12d ⊢ y = B → A ∈ Q ∧ y ∈ R ∧ z ∈ S ∧ w ∈ T → ψ ↔ A ∈ Q ∧ B ∈ R ∧ z ∈ S ∧ w ∈ T → χ
14 eleq1 ⊢ z = C → z ∈ S ↔ C ∈ S
15 14 anbi1d ⊢ z = C → z ∈ S ∧ w ∈ T ↔ C ∈ S ∧ w ∈ T
16 15 anbi2d ⊢ z = C → A ∈ Q ∧ B ∈ R ∧ z ∈ S ∧ w ∈ T ↔ A ∈ Q ∧ B ∈ R ∧ C ∈ S ∧ w ∈ T
17 16 3 imbi12d ⊢ z = C → A ∈ Q ∧ B ∈ R ∧ z ∈ S ∧ w ∈ T → χ ↔ A ∈ Q ∧ B ∈ R ∧ C ∈ S ∧ w ∈ T → ρ
18 eleq1 ⊢ w = D → w ∈ T ↔ D ∈ T
19 18 anbi2d ⊢ w = D → C ∈ S ∧ w ∈ T ↔ C ∈ S ∧ D ∈ T
20 19 anbi2d ⊢ w = D → A ∈ Q ∧ B ∈ R ∧ C ∈ S ∧ w ∈ T ↔ A ∈ Q ∧ B ∈ R ∧ C ∈ S ∧ D ∈ T
21 20 4 imbi12d ⊢ w = D → A ∈ Q ∧ B ∈ R ∧ C ∈ S ∧ w ∈ T → ρ ↔ A ∈ Q ∧ B ∈ R ∧ C ∈ S ∧ D ∈ T → θ
22 9 13 17 21 5 vtocl4g ⊢ A ∈ Q ∧ B ∈ R ∧ C ∈ S ∧ D ∈ T → A ∈ Q ∧ B ∈ R ∧ C ∈ S ∧ D ∈ T → θ
23 22 pm2.43i ⊢ A ∈ Q ∧ B ∈ R ∧ C ∈ S ∧ D ∈ T → θ