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

Theorem mp3an1 1348
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 1207 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 675 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  mp3an12  1351  mp3an1i  1354  mp3anl1  1355  mp3an  1361  onint  6642  wfrlem12  7064  wfrlem17  7069  tfrlem9  7120  oaord1  7269  oaword2  7271  oawordeulem  7272  oa00  7277  omword1  7291  omword2  7292  omlimcl  7296  oeoelem  7316  nnaordex  7356  enp1i  7821  unfilem2  7851  dffi3  7960  unbnn3  8178  pwcdaen  8628  ackbij1b  8682  zorn2  8949  zornn0  8951  ttukey  8961  brdom7disj  8972  brdom6disj  8973  wunex2  9176  muladd11  9816  00id  9821  mul02  9824  negsubdi  9943  mulneg1  10068  ltaddpos  10117  addge01  10137  reccl  10290  recid  10297  recid2  10298  recdiv2  10333  divdiv23zi  10373  ltmul12a  10474  lemul12a  10476  mulgt1  10477  ltmulgt11  10478  gt0div  10484  ge0div  10485  lediv12a  10512  ledivp1  10521  ltdiv23i  10544  ledivp1i  10545  ltdivp1i  10546  infm3  10581  infmrclOLD  10606  nngt1ne1  10649  8th4div3  10846  gtndiv  11026  nn0ind  11043  fnn0ind  11047  supminf  11263  supminfOLD  11264  xrre2  11478  qsqueeze  11507  xmulpnf1  11573  xlemul1a  11587  xrub  11610  ioorebas  11749  elfz0ubfz0  11907  expubnd  12345  le2sq2  12362  crreczi  12409  bernneq  12410  faclbnd5  12495  faclbnd6  12496  bccl  12519  hashbc  12626  ccatlid  12740  shftfval  13139  sgnp  13159  mulre  13190  sqrlem4  13315  sqrlem7  13318  sqreulem  13428  binom1p  13894  0.999...  13942  fallrisefac  14083  bpoly3  14116  fsumcube  14118  efsub  14159  efi4p  14196  sinadd  14223  cosadd  14224  cos2t  14237  cos2tsin  14238  sin01gt0  14249  cos01gt0  14250  absefib  14257  efieq1re  14258  demoivreALT  14260  rpnnen2lem4  14275  odd2np1  14370  divalglem0  14376  divalglem4  14380  divalglem9  14386  divalglem9OLD  14387  gcdcllem3  14480  gcdn0gt0  14491  gcdadd  14499  gcdmultiple  14523  algcvgblem  14541  algcvga  14543  isprm3  14638  divgcdodd  14658  coprm  14662  phibndlem  14723  opoe  14766  omoe  14767  opeo  14768  omeo  14769  pythagtriplem4  14774  pythagtriplem11  14780  pythagtriplem12  14781  pythagtriplem13  14782  pythagtriplem14  14783  infpn2  14862  1arith2  14877  vdwap0  14931  vdwap1  14932  ipolt  16410  gsumval2a  16527  f1otrspeq  17093  mplsubrglem  18668  evls1rhm  18916  cnfldneg  18999  cnflddiv  19003  cnfldmulg  19005  cnfldexp  19006  zringmulg  19051  remulg  19179  resubgval  19181  thlleval  19265  frlmsslsp  19358  neiptoptop  20151  iccordt  20234  qustgplem  21139  bl2ioo  21814  ioo2blex  21816  blssioo  21817  tgioo  21818  xrsblre  21833  iccntr  21843  icccmplem3  21846  reconnlem2  21849  opnreen  21853  iccpnfcnv  21976  cnllycmp  21988  pcoptcl  22056  ovolmge0  22434  ovolctb2  22449  ismbl2  22485  cmmbl  22492  nulmbl  22493  unmbl  22495  voliunlem1  22507  voliunlem2  22508  ioombl1  22519  opnmbllem  22563  mbfima  22592  i1fsub  22670  itg1sub  22671  ellimc3  22838  limcflf  22840  dvcnvre  22975  coe1termlem  23216  dgrsub  23230  dvnply2  23244  dvnply  23245  reeff1o  23406  sinperlem  23439  sincosq1eq  23471  resinf1o  23489  logeftb  23537  logge0  23558  logdivlti  23573  efopn  23607  logtayl2  23611  loglesqrt  23702  logrec  23704  xrlimcnp  23898  ppinncl  24105  chtrpcl  24106  bposlem2  24217  bposlem8  24223  lgsdir2  24260  1lgs  24269  brbtwn2  24939  colinearalglem4  24943  ax5seglem1  24962  ax5seglem2  24963  axcontlem2  24999  axcontlem4  25001  axcontlem7  25004  iswlkg  25256  redwlklem  25339  0vgrargra  25669  isgrpoi  25930  grpo2grp  25966  imsmetlem  26326  nmcvcn  26335  ipval2  26347  lnocoi  26402  nmlno0lem  26438  nmblolbii  26444  blometi  26448  blocnilem  26449  blocni  26450  ipasslem1  26476  ipasslem2  26477  ipasslem4  26479  ipasslem5  26480  ipasslem8  26482  ipblnfi  26501  ip2eqi  26502  ubthlem1  26516  htthlem  26574  h2hmetdval  26635  axhvcom-zf  26640  axhis1-zf  26651  axhis4-zf  26654  hvm1neg  26689  hvsub4  26694  hvsubass  26701  hvsubdistr2  26707  hv2times  26718  hvsubcan  26731  hvsubcan2  26732  his2sub  26749  norm-i  26786  normpyc  26803  hhip  26834  hhph  26835  norm1exi  26907  hhssabloi  26917  hhssnv  26919  hhshsslem2  26923  hhssmetdval  26933  shscli  26974  shunssi  27025  shsleji  27027  shsidmi  27041  spanunsni  27236  h1datomi  27238  spansncvi  27309  pjss2i  27337  pjssmii  27338  pjocini  27355  homulid2  27457  honegdi  27466  ho2times  27476  nmopge0  27568  nmopgt0  27569  nmfnge0  27584  lnopaddi  27628  lnopmuli  27629  lnopsubi  27631  hmopbdoptHIL  27645  nmbdoplbi  27681  nmcoplbi  27685  nmophmi  27688  lnopconi  27691  lnfnaddi  27700  lnfnsubi  27703  nmbdfnlbi  27706  nmcfnlbi  27709  lnfnconi  27712  imaelshi  27715  cnlnadjlem2  27725  cnlnadjlem7  27730  nmoptrii  27751  nmopcoi  27752  adjcoi  27757  nmopcoadji  27758  bracnlnval  27771  leopmul  27791  opsqrlem1  27797  opsqrlem6  27802  hmopidmpji  27809  sto2i  27894  strlem1  27907  atcveq0  28005  atcv0eq  28036  atomli  28039  atcvati  28043  atcvat3i  28053  cdjreui  28089  cdj1i  28090  xdiv0  28411  xdivpnfrp  28415  mhmhmeotmd  28747  rezh  28789  qqhucn  28810  blscon  29981  cnllyscon  29982  ghomgrpilem2  30318  ghomsn  30320  sinccvglem  30330  frrlem11  30539  nobndlem8  30599  opnrebl2  30988  ptrecube  31910  poimirlem6  31916  poimirlem7  31917  poimirlem29  31939  poimirlem30  31940  opnmbllem0  31946  mblfinlem3  31949  mblfinlem4  31950  ismblfin  31951  voliunnfl  31954  ftc1anclem5  31991  ftc1anclem6  31992  ftc1anclem7  31993  ftc1anclem8  31994  ftc1anc  31995  heiborlem7  32119  rrnequiv  32137  ismrer1  32140  cnaddcom  32513  mapco2  35532  mzpaddmpt  35558  mzpmulmpt  35559  zindbi  35770  mpaaeu  35992  eel000cT  37061  eel0TT  37062  eel011  37065  eel012  37067  fusgrfis  39160  zringsubgval  39806  aacllem  40159
  Copyright terms: Public domain W3C validator