Proof of Theorem wl-ifpimpr
Step | Hyp | Ref
| Expression |
1 | | pm4.72 948 |
. . . . . . 7
⊢ ((𝜒 → 𝜓) ↔ (𝜓 ↔ (𝜒 ∨ 𝜓))) |
2 | 1 | biimpi 219 |
. . . . . 6
⊢ ((𝜒 → 𝜓) → (𝜓 ↔ (𝜒 ∨ 𝜓))) |
3 | | orcom 868 |
. . . . . 6
⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒)) |
4 | 2, 3 | syl6bb 291 |
. . . . 5
⊢ ((𝜒 → 𝜓) → (𝜓 ↔ (𝜓 ∨ 𝜒))) |
5 | 4 | anbi2d 632 |
. . . 4
⊢ ((𝜒 → 𝜓) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒)))) |
6 | | andi 1006 |
. . . 4
⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
7 | 5, 6 | syl6bb 291 |
. . 3
⊢ ((𝜒 → 𝜓) → ((𝜑 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))) |
8 | 7 | orbi1d 915 |
. 2
⊢ ((𝜒 → 𝜓) → (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) ∨ (¬ 𝜑 ∧ 𝜒)))) |
9 | | df-ifp 1060 |
. 2
⊢
(if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
10 | | biidd 265 |
. . . . 5
⊢ (𝜑 → (𝜒 ↔ 𝜒)) |
11 | | biidd 265 |
. . . . 5
⊢ (¬
𝜑 → (𝜒 ↔ 𝜒)) |
12 | 10, 11 | cases 1039 |
. . . 4
⊢ (𝜒 ↔ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜒))) |
13 | 12 | orbi2i 911 |
. . 3
⊢ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜒)))) |
14 | | orass 920 |
. . 3
⊢ ((((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜒)))) |
15 | 13, 14 | bitr4i 281 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) ∨ (¬ 𝜑 ∧ 𝜒))) |
16 | 8, 9, 15 | 3bitr4g 318 |
1
⊢ ((𝜒 → 𝜓) → (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ 𝜒))) |