Proof of Theorem ifp1bi
Step | Hyp | Ref
| Expression |
1 | | dfbi2 467 |
. 2
⊢
((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ∧ (if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃)))) |
2 | | ifpim1g 39263 |
. . . 4
⊢
((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)))) |
3 | | ancom 453 |
. . . 4
⊢ ((((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃))) ↔ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)))) |
4 | 2, 3 | bitri 267 |
. . 3
⊢
((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)))) |
5 | | ifpim1g 39263 |
. . 3
⊢
((if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃)) ↔ (((𝜑 → 𝜓) ∨ (𝜃 → 𝜒)) ∧ ((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)))) |
6 | 4, 5 | anbi12i 617 |
. 2
⊢
(((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ∧ (if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃))) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜓) ∨ (𝜃 → 𝜒)) ∧ ((𝜓 → 𝜑) ∨ (𝜒 → 𝜃))))) |
7 | | an42 644 |
. 2
⊢
(((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜓) ∨ (𝜃 → 𝜒)) ∧ ((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)))) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))))) |
8 | 1, 6, 7 | 3bitri 289 |
1
⊢
((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))))) |