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  799  oplem1  1056  axc11n  2426  weniso  7288  infssuni  9230  ordtypelem10  9413  oismo  9426  rankval3b  9716  grur1  10708  sqeqd  15070  hausflimi  23893  minveclem4  25357  ovolunnul  25426  vitali  25539  itg2mono  25679  frgrncvvdeqlem8  30281  minvecolem4  30855  contrd  38136  fppr2odd  47761