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  799  oplem1  1052  axc11n  2449  weniso  7081  infssuni  8791  ordtypelem10  8967  oismo  8980  rankval3b  9231  grur1  10219  sqeqd  14504  hausflimi  22564  minveclem4  24015  ovolunnul  24083  vitali  24196  itg2mono  24336  frgrncvvdeqlem8  28070  minvecolem4  28642  contrd  35417  fppr2odd  44068
 Copyright terms: Public domain W3C validator