Proof of Theorem ifpororb
Step | Hyp | Ref
| Expression |
1 | | dfifp2 1064 |
. 2
⊢
(if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ ((𝜑 → (𝜓 ∨ 𝜒)) ∧ (¬ 𝜑 → (𝜃 ∨ 𝜏)))) |
2 | | df-or 847 |
. . . 4
⊢ ((𝜓 ∨ 𝜒) ↔ (¬ 𝜓 → 𝜒)) |
3 | 2 | imbi2i 339 |
. . 3
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) ↔ (𝜑 → (¬ 𝜓 → 𝜒))) |
4 | | df-or 847 |
. . . 4
⊢ ((𝜃 ∨ 𝜏) ↔ (¬ 𝜃 → 𝜏)) |
5 | 4 | imbi2i 339 |
. . 3
⊢ ((¬
𝜑 → (𝜃 ∨ 𝜏)) ↔ (¬ 𝜑 → (¬ 𝜃 → 𝜏))) |
6 | 3, 5 | anbi12i 630 |
. 2
⊢ (((𝜑 → (𝜓 ∨ 𝜒)) ∧ (¬ 𝜑 → (𝜃 ∨ 𝜏))) ↔ ((𝜑 → (¬ 𝜓 → 𝜒)) ∧ (¬ 𝜑 → (¬ 𝜃 → 𝜏)))) |
7 | | ifpimimb 40665 |
. . 3
⊢
(if-(𝜑, (¬ 𝜓 → 𝜒), (¬ 𝜃 → 𝜏)) ↔ (if-(𝜑, ¬ 𝜓, ¬ 𝜃) → if-(𝜑, 𝜒, 𝜏))) |
8 | | dfifp2 1064 |
. . 3
⊢
(if-(𝜑, (¬ 𝜓 → 𝜒), (¬ 𝜃 → 𝜏)) ↔ ((𝜑 → (¬ 𝜓 → 𝜒)) ∧ (¬ 𝜑 → (¬ 𝜃 → 𝜏)))) |
9 | | imor 852 |
. . . 4
⊢
((if-(𝜑, ¬ 𝜓, ¬ 𝜃) → if-(𝜑, 𝜒, 𝜏)) ↔ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜃) ∨ if-(𝜑, 𝜒, 𝜏))) |
10 | | ifpnot23d 40646 |
. . . . 5
⊢ (¬
if-(𝜑, ¬ 𝜓, ¬ 𝜃) ↔ if-(𝜑, 𝜓, 𝜃)) |
11 | 10 | orbi1i 913 |
. . . 4
⊢ ((¬
if-(𝜑, ¬ 𝜓, ¬ 𝜃) ∨ if-(𝜑, 𝜒, 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏))) |
12 | 9, 11 | bitri 278 |
. . 3
⊢
((if-(𝜑, ¬ 𝜓, ¬ 𝜃) → if-(𝜑, 𝜒, 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏))) |
13 | 7, 8, 12 | 3bitr3i 304 |
. 2
⊢ (((𝜑 → (¬ 𝜓 → 𝜒)) ∧ (¬ 𝜑 → (¬ 𝜃 → 𝜏))) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏))) |
14 | 1, 6, 13 | 3bitri 300 |
1
⊢
(if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏))) |