Metamath Proof Explorer
Description: Identical to pm2.21 . Proposition 38 of Frege1879 p. 46.
(Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
frege38 |
⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
frege36 |
⊢ ( 𝜑 → ( ¬ 𝜑 → 𝜓 ) ) |
2 |
|
ax-frege8 |
⊢ ( ( 𝜑 → ( ¬ 𝜑 → 𝜓 ) ) → ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) ) ) |
3 |
1 2
|
ax-mp |
⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) ) |