Theorem pm2.18d 128

Description: Deduction form of the Clavius law pm2.18 129. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) Shorten pm2.18 129. (Revised by Wolf Lammen, 17-Nov-2023.)

Hypothesis

Ref	Expression
pm2.18d.1	⊢ (𝜑 → (¬ 𝜓 → 𝜓))

Assertion

Ref	Expression
pm2.18d	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.18d

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2		pm2.18d.1	. . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝜓))
3		pm2.21 124	. . 3 ⊢ (¬ 𝜓 → (𝜓 → ¬ 𝜑))
4	2, 3	sylcom 31	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜑))
5	1, 4	mt4d 118	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.18  129  pm2.61d  181  pm2.18da  812  oplem1  1072  axc11n  2457  weniso  7361  infssuni  9317  ordtypelem10  9503  oismo  9516  rankval3b  9812  grur1  10833  sqeqd  15257  hausflimi  24212  minveclem4  25666  ovolunnul  25734  vitali  25847  itg2mono  25987  frgrncvvdeqlem8  30794  minvecolem4  31369  contrd  38853  fppr2odd  48655