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.) 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  1056  axc11n  2430  weniso  7375  infssuni  9387  ordtypelem10  9568  oismo  9581  rankval3b  9867  grur1  10861  sqeqd  15206  hausflimi  23989  minveclem4  25467  ovolunnul  25536  vitali  25649  itg2mono  25789  frgrncvvdeqlem8  30326  minvecolem4  30900  contrd  38105  fppr2odd  47723
  Copyright terms: Public domain W3C validator