Metamath Proof Explorer
Description: Deduce con1 from con3 . Proposition 32 of Frege1879 p. 44.
(Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
frege32 |
⊢ ( ( ( ¬ 𝜑 → 𝜓 ) → ( ¬ 𝜓 → ¬ ¬ 𝜑 ) ) → ( ( ¬ 𝜑 → 𝜓 ) → ( ¬ 𝜓 → 𝜑 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ax-frege31 |
⊢ ( ¬ ¬ 𝜑 → 𝜑 ) |
| 2 |
|
frege7 |
⊢ ( ( ¬ ¬ 𝜑 → 𝜑 ) → ( ( ( ¬ 𝜑 → 𝜓 ) → ( ¬ 𝜓 → ¬ ¬ 𝜑 ) ) → ( ( ¬ 𝜑 → 𝜓 ) → ( ¬ 𝜓 → 𝜑 ) ) ) ) |
| 3 |
1 2
|
ax-mp |
⊢ ( ( ( ¬ 𝜑 → 𝜓 ) → ( ¬ 𝜓 → ¬ ¬ 𝜑 ) ) → ( ( ¬ 𝜑 → 𝜓 ) → ( ¬ 𝜓 → 𝜑 ) ) ) |