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  5548  xpexr  7148  bropopvvv  7300  bropfvvvv  7302  reldmtpos  7405  zeo  11501  rpneg  11901  xrlttri  12010  difreicc  12342  nn0o1gt2  15144  cshwshashlem1  15849  gsumbagdiag  19424  psrass1lem  19425  gsumcom3fi  20254  cfinufil  21779  sizusglecusg  26415  iswspthsnon  26806  clwlkclwwlklem2a4  26963  frgrncvvdeqlem8  27286  chirredi  29381  gsummpt2co  29908  truae  30434  bj-sngltag  33096  itg2addnclem  33591  itg2addnclem3  33593  cdleme32e  36050  ntrneiiso  38706  tz6.12-afv  41574  odz2prm2pw  41800  lighneallem3  41849  lighneallem4b  41851  lindslinindsimp2lem5  42576  nnolog2flm1  42709
  Copyright terms: Public domain W3C validator