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 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.18  129  pm2.61d  181  pm2.18da  811  oplem1  1070  axc11n  2460  weniso  7342  infssuni  9291  ordtypelem10  9477  oismo  9490  rankval3b  9786  grur1  10793  sqeqd  15207  hausflimi  24098  minveclem4  25552  ovolunnul  25620  vitali  25733  itg2mono  25873  frgrncvvdeqlem8  30566  minvecolem4  31141  contrd  38608  fppr2odd  48351