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

Theorem pm2.24d 143
Description: Deduction version of pm2.24 109. (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 124 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.5  152  asymref2  5389  xpexr  6740  bropopvvv  6880  reldmtpos  6982  zeo  10973  rpneg  11278  xrlttri  11374  difreicc  11681  cshwshashlem1  14580  gsumbagdiag  18028  psrass1lem  18029  gsumcom3fi  18902  bwthOLD  19911  cfinufil  20429  sizeusglecusg  24486  clwlkisclwwlklem2a4  24784  2wlkonot3v  24875  2spthonot3v  24876  frgrancvvdeqlemB  25038  chirredi  27313  gsummpt2co  27771  truae  28215  amosym1  29891  wl-embantd  29976  itg2addnclem  30066  itg2addnclem3  30068  tz6.12-afv  32258  lindslinindsimp2lem5  33063  bj-sngltag  34541  cdleme32e  36171
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator