Proof of Theorem ifp1bi
Step | Hyp | Ref
| Expression |
1 | | dfbi2 478 |
. 2
⊢
((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ∧ (if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃)))) |
2 | | ifpim1g 40793 |
. . . 4
⊢
((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)))) |
3 | 2 | biancomi 466 |
. . 3
⊢
((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)))) |
4 | | ifpim1g 40793 |
. . 3
⊢
((if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃)) ↔ (((𝜑 → 𝜓) ∨ (𝜃 → 𝜒)) ∧ ((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)))) |
5 | 3, 4 | anbi12i 630 |
. 2
⊢
(((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ∧ (if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃))) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜓) ∨ (𝜃 → 𝜒)) ∧ ((𝜓 → 𝜑) ∨ (𝜒 → 𝜃))))) |
6 | | an42 657 |
. 2
⊢
(((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜓) ∨ (𝜃 → 𝜒)) ∧ ((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)))) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))))) |
7 | 1, 5, 6 | 3bitri 300 |
1
⊢
((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))))) |