Proof of Theorem rp-fakeanorass
Step | Hyp | Ref
| Expression |
1 | | pm1.4 868 |
. . . . . . . 8
⊢ ((𝜑 ∨ 𝜒) → (𝜒 ∨ 𝜑)) |
2 | 1 | ord 863 |
. . . . . . 7
⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜒 → 𝜑)) |
3 | | pm4.83 1024 |
. . . . . . . 8
⊢ (((𝜒 → 𝜑) ∧ (¬ 𝜒 → 𝜑)) ↔ 𝜑) |
4 | 3 | biimpi 219 |
. . . . . . 7
⊢ (((𝜒 → 𝜑) ∧ (¬ 𝜒 → 𝜑)) → 𝜑) |
5 | 2, 4 | sylan2 596 |
. . . . . 6
⊢ (((𝜒 → 𝜑) ∧ (𝜑 ∨ 𝜒)) → 𝜑) |
6 | 5 | ex 416 |
. . . . 5
⊢ ((𝜒 → 𝜑) → ((𝜑 ∨ 𝜒) → 𝜑)) |
7 | 6 | anim1d 614 |
. . . 4
⊢ ((𝜒 → 𝜑) → (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))) |
8 | | orc 866 |
. . . . 5
⊢ (𝜑 → (𝜑 ∨ 𝜒)) |
9 | 8 | anim1i 618 |
. . . 4
⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))) |
10 | 7, 9 | jctir 524 |
. . 3
⊢ ((𝜒 → 𝜑) → ((((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) ∧ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))))) |
11 | | olc 867 |
. . . . . 6
⊢ (𝜒 → (𝜑 ∨ 𝜒)) |
12 | | olc 867 |
. . . . . 6
⊢ (𝜒 → (𝜓 ∨ 𝜒)) |
13 | 11, 12 | jca 515 |
. . . . 5
⊢ (𝜒 → ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))) |
14 | | simpl 486 |
. . . . 5
⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → 𝜑) |
15 | 13, 14 | imim12i 62 |
. . . 4
⊢ ((((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) → (𝜒 → 𝜑)) |
16 | 15 | adantr 484 |
. . 3
⊢
(((((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) ∧ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)))) → (𝜒 → 𝜑)) |
17 | 10, 16 | impbii 212 |
. 2
⊢ ((𝜒 → 𝜑) ↔ ((((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) ∧ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))))) |
18 | | dfbi2 478 |
. 2
⊢ ((((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒))) ↔ ((((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) ∧ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))))) |
19 | | ordir 1006 |
. . . 4
⊢ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))) |
20 | 19 | bicomi 227 |
. . 3
⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ 𝜒)) |
21 | 20 | bibi1i 342 |
. 2
⊢ ((((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒))) ↔ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒)))) |
22 | 17, 18, 21 | 3bitr2i 302 |
1
⊢ ((𝜒 → 𝜑) ↔ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒)))) |