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  2458  weniso  7387  infssuni  9363  ordtypelem10  9548  oismo  9561  rankval3b  9863  grur1  10932  sqeqd  15362  hausflimi  24329  minveclem4  25783  ovolunnul  25851  vitali  25964  itg2mono  26104  frgrncvvdeqlem8  30937  minvecolem4  31512  contrd  39221  fppr2odd  49034