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

Theorem mp3an12 1269
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 1266 . 2  |-  ( ( ps  /\  ch )  ->  th )
51, 4mpan 652 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  ceqsralv  2951  tfi  4800  peano5  4835  brelrn  5067  funpr  5469  oneo  6791  nnneo  6861  fpm  7013  ener  7121  unxpdomlem3  7282  ackbij2  8087  ac6  8324  alephadd  8416  axgroth3  8670  axpre-sup  9008  ltnei  9161  mul02  9208  cnegex2  9212  addid2  9213  renegcli  9326  div0  9670  divclzi  9713  divcan1zi  9714  divcan2zi  9715  divreczi  9716  divcan3zi  9717  divcan4zi  9718  divasszi  9728  divmulzi  9729  divdirzi  9730  redivclzi  9744  ltm1  9814  mulgt1  9833  recgt1i  9871  recreclt  9873  ltmul1i  9893  ltdiv1i  9894  ltmuldivi  9895  ltmul2i  9896  lemul1i  9897  lemul2i  9898  ledivp1i  9900  ltdivp1i  9901  cju  9960  nnge1  9990  nngt0  9993  nnrecgt0  10001  nnunb  10181  elnnnn0c  10229  elnnz1  10271  recnz  10309  eluzsubi  10477  ge0gtmnf  10724  x2times  10842  xrub  10854  iccen  11004  1mod  11236  m1expcl2  11366  1exp  11372  expubnd  11403  iexpcyc  11448  expnbnd  11471  expnlbnd  11472  faclbnd4lem1  11547  hashfun  11663  remim  11885  imval2  11919  cjdivi  11959  resqrex  12019  sqrneglem  12035  absdivzi  12173  iseraltlem2  12439  climcndslem1  12592  climcndslem2  12593  geo2lim  12615  sinhval  12718  coshval  12719  ef01bndlem  12748  sin01gt0  12754  cos01gt0  12755  absefib  12762  efieq1re  12763  divalglem5  12880  phiprmpw  13128  oddprm  13152  pythagtriplem1  13153  pythagtriplem11  13162  pythagtriplem13  13164  vdwlem13  13324  prmlem1  13393  prmlem2  13405  ress0  13486  frmdplusg  14762  resstopn  17212  lecldbas  17245  hmphindis  17790  cnbl0  18769  xrsmopn  18804  zdis  18808  reperflem  18810  xrge0tsms  18826  xrhmeo  18932  oprpiece1res1  18937  cphsqrcl  19108  ovolicopnf  19381  voliunlem3  19407  volsup  19411  volivth  19460  itg2seq  19595  itg2monolem2  19604  itgz  19633  ibl0  19639  iblss  19657  iblss2  19658  itgss  19664  itgeqa  19666  iblconst  19670  iblabsr  19682  iblmulc2  19683  itgsplit  19688  coeidp  20142  dgrsub  20151  aaliou3lem2  20221  abelth  20318  reeff1olem  20323  pilem3  20330  sincosq1sgn  20367  sincosq3sgn  20369  sincosq4sgn  20370  sineq0  20390  resinf1o  20399  efif1olem4  20408  logdivlti  20476  logdivlt  20477  efopn  20510  1cxp  20524  ecxp  20525  cxpsqr  20555  isosctrlem1  20623  sinasin  20690  asinsin  20693  log2cnv  20745  basellem2  20825  basellem3  20826  isnsqf  20879  ppidif  20907  ppiublem1  20947  chtub  20957  efexple  21026  bposlem6  21034  bposlem8  21036  bposlem9  21037  lgsdir2lem2  21069  2sqb  21123  ostth3  21293  constr3trllem3  21600  imsmetlem  22143  nmoubi  22234  nmobndi  22237  nmounbi  22238  nmlno0lem  22255  nmlnoubi  22258  isblo3i  22263  blometi  22265  blocni  22267  blocn2  22270  ipasslem2  22294  siii  22315  ubthlem1  22333  ubthlem2  22334  ubthlem3  22335  htthlem  22381  hvsubid  22489  hv2times  22524  hi01  22559  hhssabloi  22723  pjsumi  23173  mayete3i  23191  mayete3iOLD  23192  hoaddcomi  23236  hodsi  23239  hoaddassi  23240  hocadddiri  23243  hocsubdiri  23244  hoaddid1i  23250  honegsubi  23260  honegneg  23270  ho2times  23283  eigrei  23298  eigorthi  23301  nmopnegi  23429  hoddii  23453  lnophsi  23465  lnopeqi  23472  nmoptrii  23558  opsqrlem1  23604  opsqrlem6  23609  pjsdii  23619  pjddii  23620  pjscji  23634  pjssposi  23636  pjssdif2i  23638  pjtoi  23643  mdsl2bi  23787  cvmdi  23788  mdslmd3i  23796  mdslmd4i  23797  mdexchi  23799  cvati  23830  cvexchlem  23832  mdsymi  23875  dmdbr5ati  23886  cdj1i  23897  cdj3lem1  23898  xrge0tsmsd  24184  rrhre  24348  esumpinfval  24424  probmeasb  24649  cvmliftlem5  24937  wfr3  25497  fullfunfv  25708  axpaschlem  25791  axlowdimlem3  25795  axlowdimlem7  25799  axlowdimlem9  25801  axlowdimlem12  25804  axlowdimlem16  25808  axlowdimlem17  25809  axlowdim  25812  bpoly3  26016  mblfinlem  26151  mblfinlem2  26152  mblfinlem3  26153  ismblfin  26154  volsupnfl  26158  itg2addnclem3  26165  iblmulc2nc  26177  finminlem  26219  nn0prpwlem  26223  heiborlem3  26420  heiborlem6  26423  heiborlem8  26425  isnumbasgrplem1  27142  islindf4  27184  symggen  27287  m1expaddsub  27297  psgnuni  27298  eel001  28534  cdleme32fva  30931
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator