Proof of Theorem vtocl3gafOLD
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vtocl3gaf.a | . . 3
⊢
Ⅎ𝑥𝐴 | 
| 2 |  | vtocl3gaf.b | . . 3
⊢
Ⅎ𝑦𝐴 | 
| 3 |  | vtocl3gaf.c | . . 3
⊢
Ⅎ𝑧𝐴 | 
| 4 |  | vtocl3gaf.d | . . 3
⊢
Ⅎ𝑦𝐵 | 
| 5 |  | vtocl3gaf.e | . . 3
⊢
Ⅎ𝑧𝐵 | 
| 6 |  | vtocl3gaf.f | . . 3
⊢
Ⅎ𝑧𝐶 | 
| 7 | 1 | nfel1 2921 | . . . . 5
⊢
Ⅎ𝑥 𝐴 ∈ 𝑅 | 
| 8 |  | nfv 1913 | . . . . 5
⊢
Ⅎ𝑥 𝑦 ∈ 𝑆 | 
| 9 |  | nfv 1913 | . . . . 5
⊢
Ⅎ𝑥 𝑧 ∈ 𝑇 | 
| 10 | 7, 8, 9 | nf3an 1900 | . . . 4
⊢
Ⅎ𝑥(𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) | 
| 11 |  | vtocl3gaf.1 | . . . 4
⊢
Ⅎ𝑥𝜓 | 
| 12 | 10, 11 | nfim 1895 | . . 3
⊢
Ⅎ𝑥((𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜓) | 
| 13 | 2 | nfel1 2921 | . . . . 5
⊢
Ⅎ𝑦 𝐴 ∈ 𝑅 | 
| 14 | 4 | nfel1 2921 | . . . . 5
⊢
Ⅎ𝑦 𝐵 ∈ 𝑆 | 
| 15 |  | nfv 1913 | . . . . 5
⊢
Ⅎ𝑦 𝑧 ∈ 𝑇 | 
| 16 | 13, 14, 15 | nf3an 1900 | . . . 4
⊢
Ⅎ𝑦(𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) | 
| 17 |  | vtocl3gaf.2 | . . . 4
⊢
Ⅎ𝑦𝜒 | 
| 18 | 16, 17 | nfim 1895 | . . 3
⊢
Ⅎ𝑦((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜒) | 
| 19 | 3 | nfel1 2921 | . . . . 5
⊢
Ⅎ𝑧 𝐴 ∈ 𝑅 | 
| 20 | 5 | nfel1 2921 | . . . . 5
⊢
Ⅎ𝑧 𝐵 ∈ 𝑆 | 
| 21 | 6 | nfel1 2921 | . . . . 5
⊢
Ⅎ𝑧 𝐶 ∈ 𝑇 | 
| 22 | 19, 20, 21 | nf3an 1900 | . . . 4
⊢
Ⅎ𝑧(𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) | 
| 23 |  | vtocl3gaf.3 | . . . 4
⊢
Ⅎ𝑧𝜃 | 
| 24 | 22, 23 | nfim 1895 | . . 3
⊢
Ⅎ𝑧((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃) | 
| 25 |  | eleq1 2828 | . . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑅 ↔ 𝐴 ∈ 𝑅)) | 
| 26 | 25 | 3anbi1d 1441 | . . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) ↔ (𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇))) | 
| 27 |  | vtocl3gaf.4 | . . . 4
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | 
| 28 | 26, 27 | imbi12d 344 | . . 3
⊢ (𝑥 = 𝐴 → (((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜑) ↔ ((𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜓))) | 
| 29 |  | eleq1 2828 | . . . . 5
⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆)) | 
| 30 | 29 | 3anbi2d 1442 | . . . 4
⊢ (𝑦 = 𝐵 → ((𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) ↔ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇))) | 
| 31 |  | vtocl3gaf.5 | . . . 4
⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | 
| 32 | 30, 31 | imbi12d 344 | . . 3
⊢ (𝑦 = 𝐵 → (((𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜓) ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜒))) | 
| 33 |  | eleq1 2828 | . . . . 5
⊢ (𝑧 = 𝐶 → (𝑧 ∈ 𝑇 ↔ 𝐶 ∈ 𝑇)) | 
| 34 | 33 | 3anbi3d 1443 | . . . 4
⊢ (𝑧 = 𝐶 → ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) ↔ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇))) | 
| 35 |  | vtocl3gaf.6 | . . . 4
⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) | 
| 36 | 34, 35 | imbi12d 344 | . . 3
⊢ (𝑧 = 𝐶 → (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜒) ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃))) | 
| 37 |  | vtocl3gaf.7 | . . 3
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜑) | 
| 38 | 1, 2, 3, 4, 5, 6, 12, 18, 24, 28, 32, 36, 37 | vtocl3gf 3572 | . 2
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃)) | 
| 39 | 38 | pm2.43i 52 | 1
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃) |