Proof of Theorem an6
Step | Hyp | Ref
| Expression |
1 | | df-3an 965 |
. . . 4
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
2 | | df-3an 965 |
. . . 4
⊢ ((𝜃 ∧ 𝜏 ∧ 𝜂) ↔ ((𝜃 ∧ 𝜏) ∧ 𝜂)) |
3 | 1, 2 | anbi12i 456 |
. . 3
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜃 ∧ 𝜏) ∧ 𝜂))) |
4 | | an4 576 |
. . 3
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜃 ∧ 𝜏) ∧ 𝜂)) ↔ (((𝜑 ∧ 𝜓) ∧ (𝜃 ∧ 𝜏)) ∧ (𝜒 ∧ 𝜂))) |
5 | | an4 576 |
. . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜃 ∧ 𝜏)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏))) |
6 | 5 | anbi1i 454 |
. . 3
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝜃 ∧ 𝜏)) ∧ (𝜒 ∧ 𝜂)) ↔ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) ∧ (𝜒 ∧ 𝜂))) |
7 | 3, 4, 6 | 3bitri 205 |
. 2
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) ↔ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) ∧ (𝜒 ∧ 𝜂))) |
8 | | df-3an 965 |
. 2
⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏) ∧ (𝜒 ∧ 𝜂)) ↔ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) ∧ (𝜒 ∧ 𝜂))) |
9 | 7, 8 | bitr4i 186 |
1
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏) ∧ (𝜒 ∧ 𝜂))) |