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  2815  tfi  4644  peano5  4679  brelrn  4909  funpr  5302  oneo  6579  nnneo  6649  fpm  6800  ener  6908  unxpdomlem3  7069  ackbij2  7869  ac6  8107  alephadd  8199  axgroth3  8453  axpre-sup  8791  ltnei  8943  mul02  8990  cnegex2  8994  addid2  8995  renegcli  9108  div0  9452  divclzi  9495  divcan1zi  9496  divcan2zi  9497  divreczi  9498  divcan3zi  9499  divcan4zi  9500  divasszi  9510  divmulzi  9511  divdirzi  9512  redivclzi  9526  ltm1  9596  mulgt1  9615  recgt1i  9653  recreclt  9655  ltmul1i  9675  ltdiv1i  9676  ltmuldivi  9677  ltmul2i  9678  lemul1i  9679  lemul2i  9680  ledivp1i  9682  ltdivp1i  9683  cju  9742  nnge1  9772  nngt0  9775  nnrecgt0  9783  nnunb  9961  elnnnn0c  10009  elnnz1  10049  recnz  10087  eluzsubi  10255  ge0gtmnf  10501  x2times  10619  xrub  10630  iccen  10779  1mod  10996  m1expcl2  11125  1exp  11131  expubnd  11162  iexpcyc  11207  expnbnd  11230  expnlbnd  11231  faclbnd4lem1  11306  hashfun  11389  remim  11602  imval2  11636  cjdivi  11676  resqrex  11736  sqrneglem  11752  absdivzi  11890  iseraltlem2  12155  climcndslem1  12308  climcndslem2  12309  geo2lim  12331  sinhval  12434  coshval  12435  ef01bndlem  12464  sin01gt0  12470  cos01gt0  12471  absefib  12478  efieq1re  12479  divalglem5  12596  phiprmpw  12844  oddprm  12868  pythagtriplem1  12869  pythagtriplem11  12878  pythagtriplem13  12880  vdwlem13  13040  prmlem1  13109  prmlem2  13121  ress0  13202  frmdplusg  14476  resstopn  16916  lecldbas  16949  hmphindis  17488  cnbl0  18283  xrsmopn  18318  zdis  18322  reperflem  18323  xrge0tsms  18339  xrhmeo  18444  oprpiece1res1  18449  cphsqrcl  18620  ovolicopnf  18883  voliunlem3  18909  volsup  18913  volivth  18962  itg2seq  19097  itg2monolem2  19106  itgz  19135  ibl0  19141  iblss  19159  iblss2  19160  itgss  19166  itgeqa  19168  iblconst  19172  iblabsr  19184  iblmulc2  19185  itgsplit  19190  coeidp  19644  dgrsub  19653  aaliou3lem2  19723  abelth  19817  reeff1olem  19822  pilem3  19829  sincosq1sgn  19866  sincosq3sgn  19868  sincosq4sgn  19869  sineq0  19889  resinf1o  19898  efif1olem4  19907  logdivlti  19971  logdivlt  19972  efopn  20005  1cxp  20019  ecxp  20020  cxpsqr  20050  isosctrlem1  20118  sinasin  20185  asinsin  20188  log2cnv  20240  basellem2  20319  basellem3  20320  isnsqf  20373  ppidif  20401  ppiublem1  20441  chtub  20451  efexple  20520  bposlem6  20528  bposlem8  20530  bposlem9  20531  lgsdir2lem2  20563  2sqb  20617  ostth3  20787  imsmetlem  21259  nmoubi  21350  nmobndi  21353  nmounbi  21354  nmlno0lem  21371  nmlnoubi  21374  isblo3i  21379  blometi  21381  blocni  21383  blocn2  21386  ipasslem2  21410  siii  21431  ubthlem1  21449  ubthlem2  21450  ubthlem3  21451  htthlem  21497  hvsubid  21605  hv2times  21640  hi01  21675  hhssabloi  21839  pjsumi  22289  mayete3i  22307  mayete3iOLD  22308  hoaddcomi  22352  hodsi  22355  hoaddassi  22356  hocadddiri  22359  hocsubdiri  22360  hoaddid1i  22366  honegsubi  22376  honegneg  22386  ho2times  22399  eigrei  22414  eigorthi  22417  nmopnegi  22545  hoddii  22569  lnophsi  22581  lnopeqi  22588  nmoptrii  22674  opsqrlem1  22720  opsqrlem6  22725  pjsdii  22735  pjddii  22736  pjscji  22750  pjssposi  22752  pjssdif2i  22754  pjtoi  22759  mdsl2bi  22903  cvmdi  22904  mdslmd3i  22912  mdslmd4i  22913  mdexchi  22915  cvati  22946  cvexchlem  22948  mdsymi  22991  dmdbr5ati  23002  cdj1i  23013  cdj3lem1  23014  xrge0tsmsd  23382  esumpinfval  23441  probmeasb  23633  cvmliftlem5  23820  wfr3  24275  fullfunfv  24485  axpaschlem  24568  axlowdimlem3  24572  axlowdimlem7  24576  axlowdimlem9  24578  axlowdimlem12  24581  axlowdimlem16  24585  axlowdimlem17  24586  axlowdim  24589  bpoly3  24793  repcpwti  25161  cnegvex2  25660  finminlem  26231  nn0prpwlem  26238  heiborlem3  26537  heiborlem6  26540  heiborlem8  26542  isnumbasgrplem1  27266  islindf4  27308  symggen  27411  m1expaddsub  27421  psgnuni  27422  cdleme32fva  30626
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