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  800  oplem1  1056  axc11n  2429  weniso  7374  infssuni  9384  ordtypelem10  9565  oismo  9578  rankval3b  9864  grur1  10858  sqeqd  15202  hausflimi  24004  minveclem4  25480  ovolunnul  25549  vitali  25662  itg2mono  25803  frgrncvvdeqlem8  30335  minvecolem4  30909  contrd  38084  fppr2odd  47656
  Copyright terms: Public domain W3C validator