Proof of Theorem pm4.79dc
Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . 4
⊢ ((ψ → φ) → (ψ → φ)) |
2 | | id 19 |
. . . 4
⊢ ((χ → φ) → (χ → φ)) |
3 | 1, 2 | jaoa 639 |
. . 3
⊢ (((ψ → φ) ∨ (χ → φ)) → ((ψ ∧ χ) → φ)) |
4 | | simplimdc 756 |
. . . . . 6
⊢
(DECID ψ →
(¬ (ψ → φ) → ψ)) |
5 | | pm3.3 248 |
. . . . . 6
⊢ (((ψ ∧ χ) → φ) → (ψ → (χ → φ))) |
6 | 4, 5 | syl9 66 |
. . . . 5
⊢
(DECID ψ →
(((ψ ∧
χ) → φ) → (¬ (ψ → φ) → (χ → φ)))) |
7 | | dcim 783 |
. . . . . 6
⊢
(DECID ψ →
(DECID φ →
DECID (ψ → φ))) |
8 | | pm2.54dc 789 |
. . . . . 6
⊢
(DECID (ψ →
φ) → ((¬ (ψ → φ) → (χ → φ)) → ((ψ → φ) ∨ (χ → φ)))) |
9 | 7, 8 | syl6 29 |
. . . . 5
⊢
(DECID ψ →
(DECID φ → ((¬
(ψ → φ) → (χ → φ)) → ((ψ → φ) ∨ (χ → φ))))) |
10 | 6, 9 | syl5d 62 |
. . . 4
⊢
(DECID ψ →
(DECID φ → (((ψ ∧ χ) → φ) → ((ψ → φ) ∨ (χ → φ))))) |
11 | 10 | imp 115 |
. . 3
⊢
((DECID ψ ∧ DECID φ) → (((ψ ∧ χ) → φ) → ((ψ → φ) ∨ (χ → φ)))) |
12 | 3, 11 | impbid2 131 |
. 2
⊢
((DECID ψ ∧ DECID φ) → (((ψ → φ) ∨ (χ → φ)) ↔ ((ψ ∧ χ) → φ))) |
13 | 12 | expcom 109 |
1
⊢
(DECID φ →
(DECID ψ → (((ψ → φ) ∨ (χ → φ)) ↔ ((ψ ∧ χ) → φ)))) |