Proof of Theorem ifpimim
Step | Hyp | Ref
| Expression |
1 | | pm2.521 179 |
. . . . . 6
⊢ (¬
(¬ 𝜑 → 𝜑) → (𝜑 → ¬ 𝜑)) |
2 | 1 | orim1i 909 |
. . . . 5
⊢ ((¬
(¬ 𝜑 → 𝜑) ∨ (𝜓 → 𝜒)) → ((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒))) |
3 | 2 | adantr 484 |
. . . 4
⊢ (((¬
(¬ 𝜑 → 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))) → ((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒))) |
4 | | id 22 |
. . . . . 6
⊢ (𝜑 → 𝜑) |
5 | 4 | orci 864 |
. . . . 5
⊢ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒)) |
6 | 5 | a1i 11 |
. . . 4
⊢ (((¬
(¬ 𝜑 → 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))) → ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))) |
7 | 3, 6 | jca 515 |
. . 3
⊢ (((¬
(¬ 𝜑 → 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))) → (((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒)))) |
8 | 4 | orci 864 |
. . . . 5
⊢ ((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) |
9 | 8 | a1i 11 |
. . . 4
⊢ (((¬
(¬ 𝜑 → 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))) → ((𝜑 → 𝜑) ∨ (𝜓 → 𝜏))) |
10 | | simpr 488 |
. . . 4
⊢ (((¬
(¬ 𝜑 → 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))) → ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))) |
11 | 9, 10 | jca 515 |
. . 3
⊢ (((¬
(¬ 𝜑 → 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))) → (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))) |
12 | 7, 11 | jca 515 |
. 2
⊢ (((¬
(¬ 𝜑 → 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))) → ((((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))))) |
13 | | pm4.81 397 |
. . . . 5
⊢ ((¬
𝜑 → 𝜑) ↔ 𝜑) |
14 | 13 | bicomi 227 |
. . . 4
⊢ (𝜑 ↔ (¬ 𝜑 → 𝜑)) |
15 | | ifpbi1 40678 |
. . . 4
⊢ ((𝜑 ↔ (¬ 𝜑 → 𝜑)) → (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ if-((¬ 𝜑 → 𝜑), (𝜓 → 𝜒), (𝜃 → 𝜏)))) |
16 | 14, 15 | ax-mp 5 |
. . 3
⊢
(if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ if-((¬ 𝜑 → 𝜑), (𝜓 → 𝜒), (𝜃 → 𝜏))) |
17 | | dfifp4 1066 |
. . 3
⊢
(if-((¬ 𝜑 →
𝜑), (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ ((¬ (¬ 𝜑 → 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))) |
18 | 16, 17 | bitri 278 |
. 2
⊢
(if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ ((¬ (¬ 𝜑 → 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))) |
19 | | ifpim123g 40701 |
. 2
⊢
((if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)) ↔ ((((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))))) |
20 | 12, 18, 19 | 3imtr4i 295 |
1
⊢
(if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) |