Proof of Theorem rp-fakeoranass
Step | Hyp | Ref
| Expression |
1 | | rp-fakeanorass 40852 |
. 2
⊢ ((𝜑 → 𝜒) ↔ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑)))) |
2 | | bicom 225 |
. . 3
⊢ ((((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))) ↔ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∨ 𝜑))) |
3 | | orcom 870 |
. . . . 5
⊢ ((𝜓 ∨ 𝜑) ↔ (𝜑 ∨ 𝜓)) |
4 | 3 | anbi1ci 629 |
. . . 4
⊢ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜑 ∨ 𝜓) ∧ 𝜒)) |
5 | | orcom 870 |
. . . . 5
⊢ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜑 ∨ (𝜒 ∧ 𝜓))) |
6 | | ancom 464 |
. . . . . 6
⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒)) |
7 | 6 | orbi2i 913 |
. . . . 5
⊢ ((𝜑 ∨ (𝜒 ∧ 𝜓)) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))) |
8 | 5, 7 | bitri 278 |
. . . 4
⊢ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))) |
9 | 4, 8 | bibi12i 343 |
. . 3
⊢ (((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∨ 𝜑)) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))) |
10 | 2, 9 | bitri 278 |
. 2
⊢ ((((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))) |
11 | 1, 10 | bitri 278 |
1
⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))) |