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

Theorem mp3an1 1301
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an1.1  |-  ph
mp3an1.2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an1  |-  ( ( ps  /\  ch )  ->  th )

Proof of Theorem mp3an1
StepHypRef Expression
1 mp3an1.1 . 2  |-  ph
2 mp3an1.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expb 1188 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 670 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  mp3an12  1304  mp3an1i  1307  mp3anl1  1308  mp3an  1314  onint  6411  tfrlem9  6849  oaord1  6995  oaword2  6997  oawordeulem  6998  oa00  7003  omword1  7017  omword2  7018  omlimcl  7022  oeoelem  7042  nnaordex  7082  enp1i  7552  unfilem2  7582  dffi3  7686  unbnn3  7869  pwcdaen  8359  ackbij1b  8413  zorn2  8680  zornn0  8682  ttukey  8692  brdom7disj  8703  brdom6disj  8704  wunex2  8910  muladd11  9544  00id  9549  mul02  9552  negsubdi  9670  mulneg1  9786  ltaddpos  9834  addge01  9854  reccl  10006  recid  10013  recid2  10014  recdiv2  10049  divdiv23zi  10089  ltmul12a  10190  lemul12a  10192  mulgt1  10193  ltmulgt11  10194  gt0div  10200  ge0div  10201  lediv12a  10230  ledivp1  10239  ltdiv23i  10262  ledivp1i  10263  ltdivp1i  10264  infm3  10294  infmrcl  10314  nngt1ne1  10354  8th4div3  10550  gtndiv  10724  nn0ind  10743  fnn0ind  10746  supminf  10947  xrre2  11147  qsqueeze  11176  xmulpnf1  11242  xlemul1a  11256  xrub  11279  ioorebas  11396  elfzelfzelfz  11489  expubnd  11929  le2sq2  11946  crreczi  11994  bernneq  11995  faclbnd5  12079  faclbnd6  12080  bccl  12103  hashbc  12211  ccatlid  12289  shftfval  12564  sgnp  12584  mulre  12615  sqrlem4  12740  sqrlem7  12743  sqreulem  12852  binom1p  13299  0.999...  13346  efsub  13389  efi4p  13426  sinadd  13453  cosadd  13454  cos2t  13467  cos2tsin  13468  sin01gt0  13479  cos01gt0  13480  absefib  13487  efieq1re  13488  demoivreALT  13490  rpnnen2lem4  13505  odd2np1  13597  divalglem0  13602  divalglem4  13605  divalglem9  13610  gcdcllem3  13702  gcdn0gt0  13711  gcdadd  13719  gcdmultiple  13739  algcvgblem  13757  algcvga  13759  isprm3  13777  coprm  13791  divgcdodd  13810  phibndlem  13850  opoe  13883  omoe  13884  opeo  13885  omeo  13886  pythagtriplem4  13891  pythagtriplem11  13897  pythagtriplem12  13898  pythagtriplem13  13899  pythagtriplem14  13900  infpn2  13979  1arith2  13994  vdwap0  14042  vdwap1  14043  ipolt  15334  gsumval2a  15517  f1otrspeq  15958  mplsubrglem  17522  mplsubrglemOLD  17523  evls1rhm  17762  cnfldneg  17847  cnflddiv  17851  cnfldmulg  17853  cnfldexp  17854  zringmulg  17896  zrngmulg  17902  remulg  18042  resubgval  18044  thlleval  18128  frlmsslsp  18228  frlmsslspOLD  18229  neiptoptop  18740  iccordt  18823  divstgplem  19696  bl2ioo  20374  ioo2blex  20376  blssioo  20377  tgioo  20378  xrsblre  20393  iccntr  20403  icccmplem3  20406  reconnlem2  20409  opnreen  20413  iccpnfcnv  20521  cnllycmp  20533  pcoptcl  20598  ovolmge0  20965  ovolctb2  20980  ismbl2  21015  cmmbl  21021  nulmbl  21022  unmbl  21024  voliunlem1  21036  voliunlem2  21037  ioombl1  21048  opnmbllem  21086  mbfima  21115  i1fsub  21191  itg1sub  21192  ellimc3  21359  limcflf  21361  dvcnvre  21496  coe1termlem  21730  dgrsub  21744  dvnply2  21758  dvnply  21759  reeff1o  21917  sinperlem  21947  sincosq1eq  21979  resinf1o  21997  logeftb  22037  logge0  22059  logdivlti  22074  efopn  22108  logtayl2  22112  loglesqr  22201  logrec  22220  xrlimcnp  22367  ppinncl  22517  chtrpcl  22518  bposlem2  22629  bposlem8  22635  lgsdir2  22672  1lgs  22681  brbtwn2  23156  colinearalglem4  23160  ax5seglem1  23179  ax5seglem2  23180  axcontlem2  23216  axcontlem4  23218  axcontlem7  23221  redwlklem  23509  isgrpoi  23690  grpo2grp  23726  imsmetlem  24086  nmcvcn  24095  ipval2  24107  lnocoi  24162  nmlno0lem  24198  nmblolbii  24204  blometi  24208  blocnilem  24209  blocni  24210  ipasslem1  24236  ipasslem2  24237  ipasslem4  24239  ipasslem5  24240  ipasslem8  24242  ipblnfi  24261  ip2eqi  24262  ubthlem1  24276  htthlem  24324  h2hmetdval  24385  axhvcom-zf  24390  axhis1-zf  24401  axhis4-zf  24404  hvm1neg  24439  hvsub4  24444  hvsubass  24451  hvsubdistr2  24457  hv2times  24468  hvsubcan  24481  hvsubcan2  24482  his2sub  24499  norm-i  24536  normpyc  24553  hhip  24584  hhph  24585  norm1exi  24658  hhssabloi  24668  hhssnv  24670  hhshsslem2  24674  hhssmetdval  24684  shscli  24725  shunssi  24776  shsleji  24778  shsidmi  24792  spanunsni  24987  h1datomi  24989  spansncvi  25060  pjss2i  25088  pjssmii  25089  pjocini  25106  homulid2  25209  honegdi  25218  ho2times  25228  nmopge0  25320  nmopgt0  25321  nmfnge0  25336  lnopaddi  25380  lnopmuli  25381  lnopsubi  25383  hmopbdoptHIL  25397  nmbdoplbi  25433  nmcoplbi  25437  nmophmi  25440  lnopconi  25443  lnfnaddi  25452  lnfnsubi  25455  nmbdfnlbi  25458  nmcfnlbi  25461  lnfnconi  25464  imaelshi  25467  cnlnadjlem2  25477  cnlnadjlem7  25482  nmoptrii  25503  nmopcoi  25504  adjcoi  25509  nmopcoadji  25510  bracnlnval  25523  leopmul  25543  opsqrlem1  25549  opsqrlem6  25554  hmopidmpji  25561  sto2i  25646  strlem1  25659  atcveq0  25757  atcv0eq  25788  atomli  25791  atcvati  25795  atcvat3i  25805  cdjreui  25841  cdj1i  25842  xdiv0  26109  xdivpnfrp  26113  mhmhmeotmd  26362  rezh  26405  qqhucn  26426  blscon  27138  cnllyscon  27139  ghomgrpilem2  27310  ghomsn  27312  sinccvglem  27322  fallrisefac  27533  wfrlem12  27740  frrlem11  27785  nobndlem8  27845  bpoly3  28206  fsumcube  28208  opnmbllem0  28432  mblfinlem3  28435  mblfinlem4  28436  ismblfin  28437  voliunnfl  28440  ftc1anclem5  28476  ftc1anclem6  28477  ftc1anclem7  28478  ftc1anclem8  28479  ftc1anc  28480  opnrebl2  28521  heiborlem7  28721  rrnequiv  28739  ismrer1  28742  mapco2  29056  mzpaddmpt  29082  mzpmulmpt  29083  zindbi  29292  mpaaeu  29512  iswlkg  30290  0vgrargra  30555  zringsubgval  30860  eel000cT  31432  eel0TT  31433  eel011  31436  eel012  31438  cnaddcom  32622
  Copyright terms: Public domain W3C validator