MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.24d Structured version   Visualization version   GIF version

Theorem pm2.24d 147
Description: Deduction form of pm2.24 121. (Contributed by NM, 30-Jan-2006.)
Hypothesis
Ref Expression
pm2.24d.1 (𝜑𝜓)
Assertion
Ref Expression
pm2.24d (𝜑 → (¬ 𝜓𝜒))

Proof of Theorem pm2.24d
StepHypRef Expression
1 pm2.24d.1 . . 3 (𝜑𝜓)
21a1d 25 . 2 (𝜑 → (¬ 𝜒𝜓))
32con1d 139 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.5  164  asymref2  5472  xpexr  7053  bropopvvv  7200  bropfvvvv  7202  reldmtpos  7305  zeo  11407  rpneg  11807  xrlttri  11916  difreicc  12246  nn0o1gt2  15021  cshwshashlem1  15726  gsumbagdiag  19295  psrass1lem  19296  gsumcom3fi  20125  cfinufil  21642  sizusglecusg  26246  clwlkclwwlklem2a4  26765  frgrncvvdeqlemB  27035  chirredi  29099  gsummpt2co  29562  truae  30084  bj-sngltag  32615  itg2addnclem  33090  itg2addnclem3  33092  cdleme32e  35210  ntrneiiso  37868  tz6.12-afv  40554  odz2prm2pw  40771  lighneallem3  40820  lighneallem4b  40822  lindslinindsimp2lem5  41536  nnolog2flm1  41673
  Copyright terms: Public domain W3C validator