Proof of Theorem 3orbi123VD
Step | Hyp | Ref
| Expression |
1 | | idn1 42156 |
. . . . . . 7
⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ▶ ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ) |
2 | | simp1 1135 |
. . . . . . 7
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (𝜑 ↔ 𝜓)) |
3 | 1, 2 | e1a 42209 |
. . . . . 6
⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ▶ (𝜑 ↔ 𝜓) ) |
4 | | simp2 1136 |
. . . . . . 7
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (𝜒 ↔ 𝜃)) |
5 | 1, 4 | e1a 42209 |
. . . . . 6
⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ▶ (𝜒 ↔ 𝜃) ) |
6 | | pm4.39 974 |
. . . . . . 7
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))) |
7 | 6 | ex 413 |
. . . . . 6
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)))) |
8 | 3, 5, 7 | e11 42270 |
. . . . 5
⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ▶ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) ) |
9 | | simp3 1137 |
. . . . . 6
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (𝜏 ↔ 𝜂)) |
10 | 1, 9 | e1a 42209 |
. . . . 5
⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ▶ (𝜏 ↔ 𝜂) ) |
11 | | pm4.39 974 |
. . . . . 6
⊢ ((((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) ∧ (𝜏 ↔ 𝜂)) → (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))) |
12 | 11 | ex 413 |
. . . . 5
⊢ (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) → ((𝜏 ↔ 𝜂) → (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)))) |
13 | 8, 10, 12 | e11 42270 |
. . . 4
⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ▶ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) ) |
14 | | df-3or 1087 |
. . . . 5
⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜏)) |
15 | 14 | bicomi 223 |
. . . 4
⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ (𝜑 ∨ 𝜒 ∨ 𝜏)) |
16 | | bitr3 353 |
. . . . 5
⊢ ((((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ (𝜑 ∨ 𝜒 ∨ 𝜏)) → ((((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)))) |
17 | 16 | com12 32 |
. . . 4
⊢ ((((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) → ((((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ (𝜑 ∨ 𝜒 ∨ 𝜏)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)))) |
18 | 13, 15, 17 | e10 42276 |
. . 3
⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ▶ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) ) |
19 | | df-3or 1087 |
. . . 4
⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) |
20 | 19 | bicomi 223 |
. . 3
⊢ (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) |
21 | | bitr 802 |
. . . 4
⊢ ((((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) ∧ (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))) |
22 | 21 | ex 413 |
. . 3
⊢ (((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) → ((((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)))) |
23 | 18, 20, 22 | e10 42276 |
. 2
⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ▶ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) ) |
24 | 23 | in1 42153 |
1
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))) |