MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.18d Structured version   Visualization version   GIF version

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.) Revised to 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
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 pm2.18d.1 . . 3 (𝜑 → (¬ 𝜓𝜓))
3 pm2.21 123 . . 3 𝜓 → (𝜓 → ¬ 𝜑))
42, 3sylcom 30 . 2 (𝜑 → (¬ 𝜓 → ¬ 𝜑))
51, 4mt4d 117 1 (𝜑𝜓)
Colors of variables: wff setvar class
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  182  pm2.18da  800  oplem1  1057  axc11n  2425  weniso  7168  infssuni  8972  ordtypelem10  9148  oismo  9161  rankval3b  9447  grur1  10439  sqeqd  14734  hausflimi  22882  minveclem4  24334  ovolunnul  24402  vitali  24515  itg2mono  24656  frgrncvvdeqlem8  28394  minvecolem4  28966  contrd  35997  fppr2odd  44864
  Copyright terms: Public domain W3C validator