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

Theorem mp3an12 1267
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mp3an12.1  |-  ph
mp3an12.2  |-  ps
mp3an12.3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an12  |-  ( ch 
->  th )

Proof of Theorem mp3an12
StepHypRef Expression
1 mp3an12.2 . 2  |-  ps
2 mp3an12.1 . . 3  |-  ph
3 mp3an12.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
42, 3mp3an1 1264 . 2  |-  ( ( ps  /\  ch )  ->  th )
51, 4mpan 651 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  ceqsralv  2828  tfi  4660  peano5  4695  brelrn  4925  funpr  5318  oneo  6595  nnneo  6665  fpm  6816  ener  6924  unxpdomlem3  7085  ackbij2  7885  ac6  8123  alephadd  8215  axgroth3  8469  axpre-sup  8807  ltnei  8959  mul02  9006  cnegex2  9010  addid2  9011  renegcli  9124  div0  9468  divclzi  9511  divcan1zi  9512  divcan2zi  9513  divreczi  9514  divcan3zi  9515  divcan4zi  9516  divasszi  9526  divmulzi  9527  divdirzi  9528  redivclzi  9542  ltm1  9612  mulgt1  9631  recgt1i  9669  recreclt  9671  ltmul1i  9691  ltdiv1i  9692  ltmuldivi  9693  ltmul2i  9694  lemul1i  9695  lemul2i  9696  ledivp1i  9698  ltdivp1i  9699  cju  9758  nnge1  9788  nngt0  9791  nnrecgt0  9799  nnunb  9977  elnnnn0c  10025  elnnz1  10065  recnz  10103  eluzsubi  10271  ge0gtmnf  10517  x2times  10635  xrub  10646  iccen  10795  1mod  11012  m1expcl2  11141  1exp  11147  expubnd  11178  iexpcyc  11223  expnbnd  11246  expnlbnd  11247  faclbnd4lem1  11322  hashfun  11405  remim  11618  imval2  11652  cjdivi  11692  resqrex  11752  sqrneglem  11768  absdivzi  11906  iseraltlem2  12171  climcndslem1  12324  climcndslem2  12325  geo2lim  12347  sinhval  12450  coshval  12451  ef01bndlem  12480  sin01gt0  12486  cos01gt0  12487  absefib  12494  efieq1re  12495  divalglem5  12612  phiprmpw  12860  oddprm  12884  pythagtriplem1  12885  pythagtriplem11  12894  pythagtriplem13  12896  vdwlem13  13056  prmlem1  13125  prmlem2  13137  ress0  13218  frmdplusg  14492  resstopn  16932  lecldbas  16965  hmphindis  17504  cnbl0  18299  xrsmopn  18334  zdis  18338  reperflem  18339  xrge0tsms  18355  xrhmeo  18460  oprpiece1res1  18465  cphsqrcl  18636  ovolicopnf  18899  voliunlem3  18925  volsup  18929  volivth  18978  itg2seq  19113  itg2monolem2  19122  itgz  19151  ibl0  19157  iblss  19175  iblss2  19176  itgss  19182  itgeqa  19184  iblconst  19188  iblabsr  19200  iblmulc2  19201  itgsplit  19206  coeidp  19660  dgrsub  19669  aaliou3lem2  19739  abelth  19833  reeff1olem  19838  pilem3  19845  sincosq1sgn  19882  sincosq3sgn  19884  sincosq4sgn  19885  sineq0  19905  resinf1o  19914  efif1olem4  19923  logdivlti  19987  logdivlt  19988  efopn  20021  1cxp  20035  ecxp  20036  cxpsqr  20066  isosctrlem1  20134  sinasin  20201  asinsin  20204  log2cnv  20256  basellem2  20335  basellem3  20336  isnsqf  20389  ppidif  20417  ppiublem1  20457  chtub  20467  efexple  20536  bposlem6  20544  bposlem8  20546  bposlem9  20547  lgsdir2lem2  20579  2sqb  20633  ostth3  20803  imsmetlem  21275  nmoubi  21366  nmobndi  21369  nmounbi  21370  nmlno0lem  21387  nmlnoubi  21390  isblo3i  21395  blometi  21397  blocni  21399  blocn2  21402  ipasslem2  21426  siii  21447  ubthlem1  21465  ubthlem2  21466  ubthlem3  21467  htthlem  21513  hvsubid  21621  hv2times  21656  hi01  21691  hhssabloi  21855  pjsumi  22305  mayete3i  22323  mayete3iOLD  22324  hoaddcomi  22368  hodsi  22371  hoaddassi  22372  hocadddiri  22375  hocsubdiri  22376  hoaddid1i  22382  honegsubi  22392  honegneg  22402  ho2times  22415  eigrei  22430  eigorthi  22433  nmopnegi  22561  hoddii  22585  lnophsi  22597  lnopeqi  22604  nmoptrii  22690  opsqrlem1  22736  opsqrlem6  22741  pjsdii  22751  pjddii  22752  pjscji  22766  pjssposi  22768  pjssdif2i  22770  pjtoi  22775  mdsl2bi  22919  cvmdi  22920  mdslmd3i  22928  mdslmd4i  22929  mdexchi  22931  cvati  22962  cvexchlem  22964  mdsymi  23007  dmdbr5ati  23018  cdj1i  23029  cdj3lem1  23030  xrge0tsmsd  23397  esumpinfval  23456  probmeasb  23648  cvmliftlem5  23835  wfr3  24346  fullfunfv  24557  axpaschlem  24640  axlowdimlem3  24644  axlowdimlem7  24648  axlowdimlem9  24650  axlowdimlem12  24653  axlowdimlem16  24657  axlowdimlem17  24658  axlowdim  24661  bpoly3  24865  itg2addnc  25005  iblmulc2nc  25016  repcpwti  25264  cnegvex2  25763  finminlem  26334  nn0prpwlem  26341  heiborlem3  26640  heiborlem6  26643  heiborlem8  26645  isnumbasgrplem1  27369  islindf4  27411  symggen  27514  m1expaddsub  27524  psgnuni  27525  constr3trllem3  28398  cdleme32fva  31248
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator