Proof of Theorem ifpan23
Step | Hyp | Ref
| Expression |
1 | | ifpan123g 40798 |
. 2
⊢
((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ (((¬ 𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒)) ∧ ((¬ 𝜑 ∨ 𝜃) ∧ (𝜑 ∨ 𝜏)))) |
2 | | an4 656 |
. 2
⊢ ((((¬
𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒)) ∧ ((¬ 𝜑 ∨ 𝜃) ∧ (𝜑 ∨ 𝜏))) ↔ (((¬ 𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ 𝜃)) ∧ ((𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)))) |
3 | | dfifp4 1067 |
. . 3
⊢
(if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏)) ↔ ((¬ 𝜑 ∨ (𝜓 ∧ 𝜃)) ∧ (𝜑 ∨ (𝜒 ∧ 𝜏)))) |
4 | | ordi 1006 |
. . . 4
⊢ ((¬
𝜑 ∨ (𝜓 ∧ 𝜃)) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ 𝜃))) |
5 | | ordi 1006 |
. . . 4
⊢ ((𝜑 ∨ (𝜒 ∧ 𝜏)) ↔ ((𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏))) |
6 | 4, 5 | anbi12i 630 |
. . 3
⊢ (((¬
𝜑 ∨ (𝜓 ∧ 𝜃)) ∧ (𝜑 ∨ (𝜒 ∧ 𝜏))) ↔ (((¬ 𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ 𝜃)) ∧ ((𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)))) |
7 | 3, 6 | bitr2i 279 |
. 2
⊢ ((((¬
𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ 𝜃)) ∧ ((𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏))) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏))) |
8 | 1, 2, 7 | 3bitri 300 |
1
⊢
((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏))) |