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  2455  weniso  7364  infssuni  9338  ordtypelem10  9524  oismo  9537  rankval3b  9839  grur1  10908  sqeqd  15338  hausflimi  24304  minveclem4  25758  ovolunnul  25826  vitali  25939  itg2mono  26079  frgrncvvdeqlem8  30912  minvecolem4  31487  contrd  39122  fppr2odd  48922