Proof of Theorem ifpdfbi
Step | Hyp | Ref
| Expression |
1 | | dfbi2 658 |
. 2
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
2 | | ifpim1 36832 |
. . . . 5
⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓)) |
3 | | ifpn 1016 |
. . . . 5
⊢
(if-(𝜑, 𝜓, ⊤) ↔ if-(¬ 𝜑, ⊤, 𝜓)) |
4 | 2, 3 | bitr4i 266 |
. . . 4
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ⊤)) |
5 | | ifpim2 36835 |
. . . 4
⊢ ((𝜓 → 𝜑) ↔ if-(𝜑, ⊤, ¬ 𝜓)) |
6 | 4, 5 | anbi12i 729 |
. . 3
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ (if-(𝜑, 𝜓, ⊤) ∧ if-(𝜑, ⊤, ¬ 𝜓))) |
7 | | ifpan23 36823 |
. . . 4
⊢
((if-(𝜑, 𝜓, ⊤) ∧ if-(𝜑, ⊤, ¬ 𝜓)) ↔ if-(𝜑, (𝜓 ∧ ⊤), (⊤ ∧ ¬
𝜓))) |
8 | | ancom 465 |
. . . . . 6
⊢ ((𝜓 ∧ ⊤) ↔ (⊤
∧ 𝜓)) |
9 | | truan 1492 |
. . . . . 6
⊢
((⊤ ∧ 𝜓)
↔ 𝜓) |
10 | 8, 9 | bitri 263 |
. . . . 5
⊢ ((𝜓 ∧ ⊤) ↔ 𝜓) |
11 | | truan 1492 |
. . . . 5
⊢
((⊤ ∧ ¬ 𝜓) ↔ ¬ 𝜓) |
12 | | ifpbi23 36836 |
. . . . 5
⊢ ((((𝜓 ∧ ⊤) ↔ 𝜓) ∧ ((⊤ ∧ ¬
𝜓) ↔ ¬ 𝜓)) → (if-(𝜑, (𝜓 ∧ ⊤), (⊤ ∧ ¬
𝜓)) ↔ if-(𝜑, 𝜓, ¬ 𝜓))) |
13 | 10, 11, 12 | mp2an 704 |
. . . 4
⊢
(if-(𝜑, (𝜓 ∧ ⊤), (⊤ ∧
¬ 𝜓)) ↔ if-(𝜑, 𝜓, ¬ 𝜓)) |
14 | 7, 13 | bitri 263 |
. . 3
⊢
((if-(𝜑, 𝜓, ⊤) ∧ if-(𝜑, ⊤, ¬ 𝜓)) ↔ if-(𝜑, 𝜓, ¬ 𝜓)) |
15 | 6, 14 | bitri 263 |
. 2
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ if-(𝜑, 𝜓, ¬ 𝜓)) |
16 | 1, 15 | bitri 263 |
1
⊢ ((𝜑 ↔ 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓)) |