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  2943  tfi  4792  peano5  4827  brelrn  5059  funpr  5461  oneo  6783  nnneo  6853  fpm  7005  ener  7113  unxpdomlem3  7274  ackbij2  8079  ac6  8316  alephadd  8408  axgroth3  8662  axpre-sup  9000  ltnei  9153  mul02  9200  cnegex2  9204  addid2  9205  renegcli  9318  div0  9662  divclzi  9705  divcan1zi  9706  divcan2zi  9707  divreczi  9708  divcan3zi  9709  divcan4zi  9710  divasszi  9720  divmulzi  9721  divdirzi  9722  redivclzi  9736  ltm1  9806  mulgt1  9825  recgt1i  9863  recreclt  9865  ltmul1i  9885  ltdiv1i  9886  ltmuldivi  9887  ltmul2i  9888  lemul1i  9889  lemul2i  9890  ledivp1i  9892  ltdivp1i  9893  cju  9952  nnge1  9982  nngt0  9985  nnrecgt0  9993  nnunb  10173  elnnnn0c  10221  elnnz1  10263  recnz  10301  eluzsubi  10469  ge0gtmnf  10716  x2times  10834  xrub  10846  iccen  10996  1mod  11228  m1expcl2  11358  1exp  11364  expubnd  11395  iexpcyc  11440  expnbnd  11463  expnlbnd  11464  faclbnd4lem1  11539  hashfun  11655  remim  11877  imval2  11911  cjdivi  11951  resqrex  12011  sqrneglem  12027  absdivzi  12165  iseraltlem2  12431  climcndslem1  12584  climcndslem2  12585  geo2lim  12607  sinhval  12710  coshval  12711  ef01bndlem  12740  sin01gt0  12746  cos01gt0  12747  absefib  12754  efieq1re  12755  divalglem5  12872  phiprmpw  13120  oddprm  13144  pythagtriplem1  13145  pythagtriplem11  13154  pythagtriplem13  13156  vdwlem13  13316  prmlem1  13385  prmlem2  13397  ress0  13478  frmdplusg  14754  resstopn  17204  lecldbas  17237  hmphindis  17782  cnbl0  18761  xrsmopn  18796  zdis  18800  reperflem  18802  xrge0tsms  18818  xrhmeo  18924  oprpiece1res1  18929  cphsqrcl  19100  ovolicopnf  19373  voliunlem3  19399  volsup  19403  volivth  19452  itg2seq  19587  itg2monolem2  19596  itgz  19625  ibl0  19631  iblss  19649  iblss2  19650  itgss  19656  itgeqa  19658  iblconst  19662  iblabsr  19674  iblmulc2  19675  itgsplit  19680  coeidp  20134  dgrsub  20143  aaliou3lem2  20213  abelth  20310  reeff1olem  20315  pilem3  20322  sincosq1sgn  20359  sincosq3sgn  20361  sincosq4sgn  20362  sineq0  20382  resinf1o  20391  efif1olem4  20400  logdivlti  20468  logdivlt  20469  efopn  20502  1cxp  20516  ecxp  20517  cxpsqr  20547  isosctrlem1  20615  sinasin  20682  asinsin  20685  log2cnv  20737  basellem2  20817  basellem3  20818  isnsqf  20871  ppidif  20899  ppiublem1  20939  chtub  20949  efexple  21018  bposlem6  21026  bposlem8  21028  bposlem9  21029  lgsdir2lem2  21061  2sqb  21115  ostth3  21285  constr3trllem3  21592  imsmetlem  22135  nmoubi  22226  nmobndi  22229  nmounbi  22230  nmlno0lem  22247  nmlnoubi  22250  isblo3i  22255  blometi  22257  blocni  22259  blocn2  22262  ipasslem2  22286  siii  22307  ubthlem1  22325  ubthlem2  22326  ubthlem3  22327  htthlem  22373  hvsubid  22481  hv2times  22516  hi01  22551  hhssabloi  22715  pjsumi  23165  mayete3i  23183  mayete3iOLD  23184  hoaddcomi  23228  hodsi  23231  hoaddassi  23232  hocadddiri  23235  hocsubdiri  23236  hoaddid1i  23242  honegsubi  23252  honegneg  23262  ho2times  23275  eigrei  23290  eigorthi  23293  nmopnegi  23421  hoddii  23445  lnophsi  23457  lnopeqi  23464  nmoptrii  23550  opsqrlem1  23596  opsqrlem6  23601  pjsdii  23611  pjddii  23612  pjscji  23626  pjssposi  23628  pjssdif2i  23630  pjtoi  23635  mdsl2bi  23779  cvmdi  23780  mdslmd3i  23788  mdslmd4i  23789  mdexchi  23791  cvati  23822  cvexchlem  23824  mdsymi  23867  dmdbr5ati  23878  cdj1i  23889  cdj3lem1  23890  xrge0tsmsd  24176  rrhre  24340  esumpinfval  24416  probmeasb  24641  cvmliftlem5  24929  wfr3  25489  fullfunfv  25700  axpaschlem  25783  axlowdimlem3  25787  axlowdimlem7  25791  axlowdimlem9  25793  axlowdimlem12  25796  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  bpoly3  26008  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  volsupnfl  26150  itg2addnclem3  26157  iblmulc2nc  26169  finminlem  26211  nn0prpwlem  26215  heiborlem3  26412  heiborlem6  26415  heiborlem8  26417  isnumbasgrplem1  27134  islindf4  27176  symggen  27279  m1expaddsub  27289  psgnuni  27290  eel001  28525  cdleme32fva  30919
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