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  179  pm2.18da  799  oplem1  1055  axc11n  2421  weniso  7356  infssuni  9361  ordtypelem10  9544  oismo  9557  rankval3b  9843  grur1  10837  sqeqd  15139  hausflimi  23877  minveclem4  25353  ovolunnul  25422  vitali  25535  itg2mono  25676  frgrncvvdeqlem8  30109  minvecolem4  30683  contrd  37564  fppr2odd  47065
  Copyright terms: Public domain W3C validator