Metamath Proof Explorer
Description: Similar to a commuted pm2.62 . Proposition 44 of Frege1879 p. 47.
(Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
frege44 |
⊢ ( ( ¬ 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → 𝜑 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
frege43 |
⊢ ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 ) |
2 |
|
frege21 |
⊢ ( ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 ) → ( ( ¬ 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → 𝜑 ) ) ) |
3 |
1 2
|
ax-mp |
⊢ ( ( ¬ 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → 𝜑 ) ) |