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

Theorem pm2.61d 158
Description: Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
Hypotheses
Ref Expression
pm2.61d.1
pm2.61d.2
Assertion
Ref Expression
pm2.61d

Proof of Theorem pm2.61d
StepHypRef Expression
1 pm2.61d.2 . . . 4
21con1d 124 . . 3
3 pm2.61d.1 . . 3
42, 3syld 44 . 2
54pm2.18d 111 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.61d1  159  pm2.61d2  160  pm5.21ndd  354  bija  355  pm2.61dan  791  ecase3d  943  axc11nlem  1938  axc11nlemOLD  2048  pm2.61dne  2774  ordunidif  4931  dff3  6044  tfindsg  6695  findsg  6727  brtpos  6983  omwordi  7239  omass  7248  nnmwordi  7303  pssnn  7758  frfi  7785  ixpiunwdom  8038  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  infxpenlem  8412  infxp  8616  ackbij1lem16  8636  axpowndlem3  8996  pwfseqlem4a  9060  gchina  9098  prlem936  9446  supsrlem  9509  flflp1  11944  hashunx  12454  swrdccat3blem  12720  repswswrd  12756  sumss  13546  fsumss  13547  prodss  13754  fprodss  13755  ruclem2  13965  prmind2  14228  rpexp  14261  fermltl  14314  prmreclem5  14438  ramcl  14547  wunress  14696  divsfval  14944  efgsfo  16757  lt6abl  16897  gsumval3OLD  16908  gsumval3  16911  mdetunilem8  19121  ordtrest2lem  19704  ptpjpre1  20072  fbfinnfr  20342  filufint  20421  ptcmplem2  20553  cphsqrtcl3  21634  ovoliun  21916  voliunlem3  21962  volsup  21966  cxpsqrt  23084  amgm  23320  wilthlem2  23343  sqff1o  23456  chtublem  23486  bposlem1  23559  bposlem3  23561  ostth  23824  clwwisshclwwlem1  24805  atdmd  27317  atmd2  27319  mdsymlem4  27325  ordtrest2NEWlem  27904  eulerpartlemb  28307  dfon2lem9  29223  ltflcei  30043  nn0prpwlem  30140  dgrsub2  31084  bj-axc11nlemv  34315  lplnexllnN  35288  2llnjaN  35290  paddasslem14  35557  cdleme32le  36173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator