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  2456  weniso  7356  infssuni  9319  ordtypelem10  9505  oismo  9518  rankval3b  9817  grur1  10886  sqeqd  15313  hausflimi  24279  minveclem4  25733  ovolunnul  25801  vitali  25914  itg2mono  26054  frgrncvvdeqlem8  30889  minvecolem4  31464  contrd  38997  fppr2odd  48773