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  2919  tfi  4766  peano5  4801  brelrn  5033  funpr  5435  oneo  6753  nnneo  6823  fpm  6975  ener  7083  unxpdomlem3  7244  ackbij2  8049  ac6  8286  alephadd  8378  axgroth3  8632  axpre-sup  8970  ltnei  9122  mul02  9169  cnegex2  9173  addid2  9174  renegcli  9287  div0  9631  divclzi  9674  divcan1zi  9675  divcan2zi  9676  divreczi  9677  divcan3zi  9678  divcan4zi  9679  divasszi  9689  divmulzi  9690  divdirzi  9691  redivclzi  9705  ltm1  9775  mulgt1  9794  recgt1i  9832  recreclt  9834  ltmul1i  9854  ltdiv1i  9855  ltmuldivi  9856  ltmul2i  9857  lemul1i  9858  lemul2i  9859  ledivp1i  9861  ltdivp1i  9862  cju  9921  nnge1  9951  nngt0  9954  nnrecgt0  9962  nnunb  10142  elnnnn0c  10190  elnnz1  10232  recnz  10270  eluzsubi  10438  ge0gtmnf  10685  x2times  10803  xrub  10815  iccen  10965  1mod  11193  m1expcl2  11323  1exp  11329  expubnd  11360  iexpcyc  11405  expnbnd  11428  expnlbnd  11429  faclbnd4lem1  11504  hashfun  11620  remim  11842  imval2  11876  cjdivi  11916  resqrex  11976  sqrneglem  11992  absdivzi  12130  iseraltlem2  12396  climcndslem1  12549  climcndslem2  12550  geo2lim  12572  sinhval  12675  coshval  12676  ef01bndlem  12705  sin01gt0  12711  cos01gt0  12712  absefib  12719  efieq1re  12720  divalglem5  12837  phiprmpw  13085  oddprm  13109  pythagtriplem1  13110  pythagtriplem11  13119  pythagtriplem13  13121  vdwlem13  13281  prmlem1  13350  prmlem2  13362  ress0  13443  frmdplusg  14719  resstopn  17165  lecldbas  17198  hmphindis  17743  cnbl0  18672  xrsmopn  18707  zdis  18711  reperflem  18713  xrge0tsms  18729  xrhmeo  18835  oprpiece1res1  18840  cphsqrcl  19011  ovolicopnf  19280  voliunlem3  19306  volsup  19310  volivth  19359  itg2seq  19494  itg2monolem2  19503  itgz  19532  ibl0  19538  iblss  19556  iblss2  19557  itgss  19563  itgeqa  19565  iblconst  19569  iblabsr  19581  iblmulc2  19582  itgsplit  19587  coeidp  20041  dgrsub  20050  aaliou3lem2  20120  abelth  20217  reeff1olem  20222  pilem3  20229  sincosq1sgn  20266  sincosq3sgn  20268  sincosq4sgn  20269  sineq0  20289  resinf1o  20298  efif1olem4  20307  logdivlti  20375  logdivlt  20376  efopn  20409  1cxp  20423  ecxp  20424  cxpsqr  20454  isosctrlem1  20522  sinasin  20589  asinsin  20592  log2cnv  20644  basellem2  20724  basellem3  20725  isnsqf  20778  ppidif  20806  ppiublem1  20846  chtub  20856  efexple  20925  bposlem6  20933  bposlem8  20935  bposlem9  20936  lgsdir2lem2  20968  2sqb  21022  ostth3  21192  constr3trllem3  21480  imsmetlem  22023  nmoubi  22114  nmobndi  22117  nmounbi  22118  nmlno0lem  22135  nmlnoubi  22138  isblo3i  22143  blometi  22145  blocni  22147  blocn2  22150  ipasslem2  22174  siii  22195  ubthlem1  22213  ubthlem2  22214  ubthlem3  22215  htthlem  22261  hvsubid  22369  hv2times  22404  hi01  22439  hhssabloi  22603  pjsumi  23053  mayete3i  23071  mayete3iOLD  23072  hoaddcomi  23116  hodsi  23119  hoaddassi  23120  hocadddiri  23123  hocsubdiri  23124  hoaddid1i  23130  honegsubi  23140  honegneg  23150  ho2times  23163  eigrei  23178  eigorthi  23181  nmopnegi  23309  hoddii  23333  lnophsi  23345  lnopeqi  23352  nmoptrii  23438  opsqrlem1  23484  opsqrlem6  23489  pjsdii  23499  pjddii  23500  pjscji  23514  pjssposi  23516  pjssdif2i  23518  pjtoi  23523  mdsl2bi  23667  cvmdi  23668  mdslmd3i  23676  mdslmd4i  23677  mdexchi  23679  cvati  23710  cvexchlem  23712  mdsymi  23755  dmdbr5ati  23766  cdj1i  23777  cdj3lem1  23778  xrge0tsmsd  24045  rrhre  24176  esumpinfval  24252  probmeasb  24460  cvmliftlem5  24748  wfr3  25292  fullfunfv  25503  axpaschlem  25586  axlowdimlem3  25590  axlowdimlem7  25594  axlowdimlem9  25596  axlowdimlem12  25599  axlowdimlem16  25603  axlowdimlem17  25604  axlowdim  25607  bpoly3  25811  volsupnfl  25949  itg2addnc  25952  iblmulc2nc  25963  finminlem  26005  nn0prpwlem  26009  heiborlem3  26206  heiborlem6  26209  heiborlem8  26211  isnumbasgrplem1  26928  islindf4  26970  symggen  27073  m1expaddsub  27083  psgnuni  27084  eel001  28150  cdleme32fva  30602
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