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

Theorem mp3an12 1270
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 1267 . 2  |-  ( ( ps  /\  ch )  ->  th )
51, 4mpan 653 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  ceqsralv  2984  tfi  4834  peano5  4869  brelrn  5101  funpr  5503  oneo  6825  nnneo  6895  fpm  7047  ener  7155  unxpdomlem3  7316  ackbij2  8124  ac6  8361  alephadd  8453  axgroth3  8707  axpre-sup  9045  ltnei  9198  mul02  9245  cnegex2  9249  addid2  9250  renegcli  9363  div0  9707  divclzi  9750  divcan1zi  9751  divcan2zi  9752  divreczi  9753  divcan3zi  9754  divcan4zi  9755  divasszi  9765  divmulzi  9766  divdirzi  9767  redivclzi  9781  ltm1  9851  mulgt1  9870  recgt1i  9908  recreclt  9910  ltmul1i  9930  ltdiv1i  9931  ltmuldivi  9932  ltmul2i  9933  lemul1i  9934  lemul2i  9935  ledivp1i  9937  ltdivp1i  9938  cju  9997  nnge1  10027  nngt0  10030  nnrecgt0  10038  nnunb  10218  elnnnn0c  10266  elnnz1  10308  recnz  10346  eluzsubi  10514  ge0gtmnf  10761  x2times  10879  xrub  10891  iccen  11041  1mod  11274  m1expcl2  11404  1exp  11410  expubnd  11441  iexpcyc  11486  expnbnd  11509  expnlbnd  11510  faclbnd4lem1  11585  hashfun  11701  remim  11923  imval2  11957  cjdivi  11997  resqrex  12057  sqrneglem  12073  absdivzi  12211  iseraltlem2  12477  climcndslem1  12630  climcndslem2  12631  geo2lim  12653  sinhval  12756  coshval  12757  ef01bndlem  12786  sin01gt0  12792  cos01gt0  12793  absefib  12800  efieq1re  12801  divalglem5  12918  phiprmpw  13166  oddprm  13190  pythagtriplem1  13191  pythagtriplem11  13200  pythagtriplem13  13202  vdwlem13  13362  prmlem1  13431  prmlem2  13443  ress0  13524  frmdplusg  14800  resstopn  17251  lecldbas  17284  hmphindis  17830  cnbl0  18809  xrsmopn  18844  zdis  18848  reperflem  18850  xrge0tsms  18866  xrhmeo  18972  oprpiece1res1  18977  cphsqrcl  19148  ovolicopnf  19421  voliunlem3  19447  volsup  19451  volivth  19500  itg2seq  19635  itg2monolem2  19644  itgz  19673  ibl0  19679  iblss  19697  iblss2  19698  itgss  19704  itgeqa  19706  iblconst  19710  iblabsr  19722  iblmulc2  19723  itgsplit  19728  coeidp  20182  dgrsub  20191  aaliou3lem2  20261  abelth  20358  reeff1olem  20363  pilem3  20370  sincosq1sgn  20407  sincosq3sgn  20409  sincosq4sgn  20410  sineq0  20430  resinf1o  20439  efif1olem4  20448  logdivlti  20516  logdivlt  20517  efopn  20550  1cxp  20564  ecxp  20565  cxpsqr  20595  isosctrlem1  20663  sinasin  20730  asinsin  20733  log2cnv  20785  basellem2  20865  basellem3  20866  isnsqf  20919  ppidif  20947  ppiublem1  20987  chtub  20997  efexple  21066  bposlem6  21074  bposlem8  21076  bposlem9  21077  lgsdir2lem2  21109  2sqb  21163  ostth3  21333  constr3trllem3  21640  imsmetlem  22183  nmoubi  22274  nmobndi  22277  nmounbi  22278  nmlno0lem  22295  nmlnoubi  22298  isblo3i  22303  blometi  22305  blocni  22307  blocn2  22310  ipasslem2  22334  siii  22355  ubthlem1  22373  ubthlem2  22374  ubthlem3  22375  htthlem  22421  hvsubid  22529  hv2times  22564  hi01  22599  hhssabloi  22763  pjsumi  23213  mayete3i  23231  mayete3iOLD  23232  hoaddcomi  23276  hodsi  23279  hoaddassi  23280  hocadddiri  23283  hocsubdiri  23284  hoaddid1i  23290  honegsubi  23300  honegneg  23310  ho2times  23323  eigrei  23338  eigorthi  23341  nmopnegi  23469  hoddii  23493  lnophsi  23505  lnopeqi  23512  nmoptrii  23598  opsqrlem1  23644  opsqrlem6  23649  pjsdii  23659  pjddii  23660  pjscji  23674  pjssposi  23676  pjssdif2i  23678  pjtoi  23683  mdsl2bi  23827  cvmdi  23828  mdslmd3i  23836  mdslmd4i  23837  mdexchi  23839  cvati  23870  cvexchlem  23872  mdsymi  23915  dmdbr5ati  23926  cdj1i  23937  cdj3lem1  23938  xrge0tsmsd  24224  rrhre  24388  esumpinfval  24464  probmeasb  24689  cvmliftlem5  24977  predeq3  25444  wrecseq3  25537  wfr3  25557  wsuceq3  25569  fullfunfv  25793  axpaschlem  25880  axlowdimlem3  25884  axlowdimlem7  25888  axlowdimlem9  25890  axlowdimlem12  25893  axlowdimlem16  25897  axlowdimlem17  25898  axlowdim  25901  bpoly3  26105  mblfinlem1  26244  mblfinlem2  26245  mblfinlem3  26246  mblfinlem4  26247  ismblfin  26248  volsupnfl  26252  itg2addnclem3  26259  iblmulc2nc  26271  ftc1anc  26289  finminlem  26322  nn0prpwlem  26326  heiborlem3  26523  heiborlem6  26526  heiborlem8  26528  isnumbasgrplem1  27244  islindf4  27286  symggen  27389  m1expaddsub  27399  psgnuni  27400  eel001  28817  cdleme32fva  31235
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator