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  2428  weniso  7294  infssuni  9237  ordtypelem10  9420  oismo  9433  rankval3b  9726  grur1  10718  sqeqd  15075  hausflimi  23896  minveclem4  25360  ovolunnul  25429  vitali  25542  itg2mono  25682  frgrncvvdeqlem8  30288  minvecolem4  30862  contrd  38157  fppr2odd  47855