Theorem pm2.18d 127

Description: Deduction form of the Clavius law pm2.18 128. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) Shorten pm2.18 128. (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 22	. 2 ⊢ (𝜑 → 𝜑)
2		pm2.18d.1	. . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝜓))
3		pm2.21 123	. . 3 ⊢ (¬ 𝜓 → (𝜓 → ¬ 𝜑))
4	2, 3	sylcom 30	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜑))
5	1, 4	mt4d 117	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  128  pm2.61d  179  pm2.18da  800  oplem1  1057  axc11n  2431  weniso  7302  infssuni  9249  ordtypelem10  9435  oismo  9448  rankval3b  9741  grur1  10734  sqeqd  15119  hausflimi  23955  minveclem4  25409  ovolunnul  25477  vitali  25590  itg2mono  25730  frgrncvvdeqlem8  30391  minvecolem4  30966  contrd  38432  fppr2odd  48219