Proof of Theorem ifpor123g
Step | Hyp | Ref
| Expression |
1 | | df-or 846 |
. . . 4
⊢
((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ (¬ if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂))) |
2 | | ifpnot23 40544 |
. . . . 5
⊢ (¬
if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜑, ¬ 𝜒, ¬ 𝜏)) |
3 | 2 | imbi1i 354 |
. . . 4
⊢ ((¬
if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ (if-(𝜑, ¬ 𝜒, ¬ 𝜏) → if-(𝜓, 𝜃, 𝜂))) |
4 | 1, 3 | bitri 278 |
. . 3
⊢
((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ (if-(𝜑, ¬ 𝜒, ¬ 𝜏) → if-(𝜓, 𝜃, 𝜂))) |
5 | | ifpim123g 40566 |
. . 3
⊢
((if-(𝜑, ¬ 𝜒, ¬ 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (¬ 𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (¬ 𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (¬ 𝜏 → 𝜂))))) |
6 | 4, 5 | bitri 278 |
. 2
⊢
((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (¬ 𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (¬ 𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (¬ 𝜏 → 𝜂))))) |
7 | | pm4.64 847 |
. . . . 5
⊢ ((¬
𝜒 → 𝜃) ↔ (𝜒 ∨ 𝜃)) |
8 | 7 | orbi2i 911 |
. . . 4
⊢ (((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒 → 𝜃)) ↔ ((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃))) |
9 | | pm4.64 847 |
. . . . 5
⊢ ((¬
𝜏 → 𝜃) ↔ (𝜏 ∨ 𝜃)) |
10 | 9 | orbi2i 911 |
. . . 4
⊢ (((𝜓 → 𝜑) ∨ (¬ 𝜏 → 𝜃)) ↔ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) |
11 | 8, 10 | anbi12i 630 |
. . 3
⊢ ((((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (¬ 𝜏 → 𝜃))) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃)))) |
12 | | pm4.64 847 |
. . . . 5
⊢ ((¬
𝜒 → 𝜂) ↔ (𝜒 ∨ 𝜂)) |
13 | 12 | orbi2i 911 |
. . . 4
⊢ (((𝜑 → 𝜓) ∨ (¬ 𝜒 → 𝜂)) ↔ ((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂))) |
14 | | pm4.64 847 |
. . . . 5
⊢ ((¬
𝜏 → 𝜂) ↔ (𝜏 ∨ 𝜂)) |
15 | 14 | orbi2i 911 |
. . . 4
⊢ (((¬
𝜓 → 𝜑) ∨ (¬ 𝜏 → 𝜂)) ↔ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂))) |
16 | 13, 15 | anbi12i 630 |
. . 3
⊢ ((((𝜑 → 𝜓) ∨ (¬ 𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (¬ 𝜏 → 𝜂))) ↔ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂)))) |
17 | 11, 16 | anbi12i 630 |
. 2
⊢
(((((𝜑 → ¬
𝜓) ∨ (¬ 𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (¬ 𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (¬ 𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (¬ 𝜏 → 𝜂)))) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂))))) |
18 | 6, 17 | bitri 278 |
1
⊢
((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂))))) |