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 125. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypothesis
Ref Expression
pm2.18d.1 (𝜑 → (¬ 𝜓𝜓))
Assertion
Ref Expression
pm2.18d (𝜑𝜓)

Proof of Theorem pm2.18d
StepHypRef Expression
1 pm2.18d.1 . 2 (𝜑 → (¬ 𝜓𝜓))
2 pm2.18 125 . 2 ((¬ 𝜓𝜓) → 𝜓)
31, 2syl 17 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.61d  172  pm2.18da  790  oplem1  1040  axc11n  2392  weniso  6876  infssuni  8545  ordtypelem10  8721  oismo  8734  rankval3b  8986  grur1  9977  sqeqd  14313  hausflimi  22192  minveclem4  23638  ovolunnul  23704  vitali  23817  itg2mono  23957  pilem3OLD  24645  frgrncvvdeqlem8  27714  minvecolem4  28308  contrd  34522
  Copyright terms: Public domain W3C validator