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

Theorem mp3an1 1296
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 1183 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 665 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 962
This theorem is referenced by:  mp3an12  1299  mp3an1i  1302  mp3anl1  1303  mp3an  1309  onint  6405  tfrlem9  6840  oaord1  6986  oaword2  6988  oawordeulem  6989  oa00  6994  omword1  7008  omword2  7009  omlimcl  7013  oeoelem  7033  nnaordex  7073  enp1i  7543  unfilem2  7573  dffi3  7677  unbnn3  7860  pwcdaen  8350  ackbij1b  8404  zorn2  8671  zornn0  8673  ttukey  8683  brdom7disj  8694  brdom6disj  8695  wunex2  8901  muladd11  9535  00id  9540  mul02  9543  negsubdi  9661  mulneg1  9777  ltaddpos  9825  addge01  9845  reccl  9997  recid  10004  recid2  10005  recdiv2  10040  divdiv23zi  10080  ltmul12a  10181  lemul12a  10183  mulgt1  10184  ltmulgt11  10185  gt0div  10191  ge0div  10192  lediv12a  10221  ledivp1  10230  ltdiv23i  10253  ledivp1i  10254  ltdivp1i  10255  infm3  10285  infmrcl  10305  nngt1ne1  10345  8th4div3  10541  gtndiv  10715  nn0ind  10734  fnn0ind  10737  supminf  10938  xrre2  11138  qsqueeze  11167  xmulpnf1  11233  xlemul1a  11247  xrub  11270  ioorebas  11387  elfzelfzelfz  11480  expubnd  11920  le2sq2  11937  crreczi  11985  bernneq  11986  faclbnd5  12070  faclbnd6  12071  bccl  12094  hashbc  12202  ccatlid  12280  shftfval  12555  sgnp  12575  mulre  12606  sqrlem4  12731  sqrlem7  12734  sqreulem  12843  binom1p  13290  0.999...  13337  efsub  13380  efi4p  13417  sinadd  13444  cosadd  13445  cos2t  13458  cos2tsin  13459  sin01gt0  13470  cos01gt0  13471  absefib  13478  efieq1re  13479  demoivreALT  13481  rpnnen2lem4  13496  odd2np1  13588  divalglem0  13593  divalglem4  13596  divalglem9  13601  gcdcllem3  13693  gcdn0gt0  13702  gcdadd  13710  gcdmultiple  13730  algcvgblem  13748  algcvga  13750  isprm3  13768  coprm  13782  divgcdodd  13801  phibndlem  13841  opoe  13874  omoe  13875  opeo  13876  omeo  13877  pythagtriplem4  13882  pythagtriplem11  13888  pythagtriplem12  13889  pythagtriplem13  13890  pythagtriplem14  13891  infpn2  13970  1arith2  13985  vdwap0  14033  vdwap1  14034  ipolt  15325  gsumval2a  15505  f1otrspeq  15946  mplsubrglem  17495  mplsubrglemOLD  17496  evls1rhm  17730  cnfldneg  17801  cnflddiv  17805  cnfldmulg  17807  cnfldexp  17808  zringmulg  17850  zrngmulg  17856  remulg  17996  resubgval  17998  thlleval  18082  frlmsslsp  18182  frlmsslspOLD  18183  neiptoptop  18694  iccordt  18777  divstgplem  19650  bl2ioo  20328  ioo2blex  20330  blssioo  20331  tgioo  20332  xrsblre  20347  iccntr  20357  icccmplem3  20360  reconnlem2  20363  opnreen  20367  iccpnfcnv  20475  cnllycmp  20487  pcoptcl  20552  ovolmge0  20919  ovolctb2  20934  ismbl2  20969  cmmbl  20975  nulmbl  20976  unmbl  20978  voliunlem1  20990  voliunlem2  20991  ioombl1  21002  opnmbllem  21040  mbfima  21069  i1fsub  21145  itg1sub  21146  ellimc3  21313  limcflf  21315  dvcnvre  21450  coe1termlem  21684  dgrsub  21698  dvnply2  21712  dvnply  21713  reeff1o  21871  sinperlem  21901  sincosq1eq  21933  resinf1o  21951  logeftb  21991  logge0  22013  logdivlti  22028  efopn  22062  logtayl2  22066  loglesqr  22155  logrec  22174  xrlimcnp  22321  ppinncl  22471  chtrpcl  22472  bposlem2  22583  bposlem8  22589  lgsdir2  22626  1lgs  22635  brbtwn2  23086  colinearalglem4  23090  ax5seglem1  23109  ax5seglem2  23110  axcontlem2  23146  axcontlem4  23148  axcontlem7  23151  redwlklem  23439  isgrpoi  23620  grpo2grp  23656  imsmetlem  24016  nmcvcn  24025  ipval2  24037  lnocoi  24092  nmlno0lem  24128  nmblolbii  24134  blometi  24138  blocnilem  24139  blocni  24140  ipasslem1  24166  ipasslem2  24167  ipasslem4  24169  ipasslem5  24170  ipasslem8  24172  ipblnfi  24191  ip2eqi  24192  ubthlem1  24206  htthlem  24254  h2hmetdval  24315  axhvcom-zf  24320  axhis1-zf  24331  axhis4-zf  24334  hvm1neg  24369  hvsub4  24374  hvsubass  24381  hvsubdistr2  24387  hv2times  24398  hvsubcan  24411  hvsubcan2  24412  his2sub  24429  norm-i  24466  normpyc  24483  hhip  24514  hhph  24515  norm1exi  24588  hhssabloi  24598  hhssnv  24600  hhshsslem2  24604  hhssmetdval  24614  shscli  24655  shunssi  24706  shsleji  24708  shsidmi  24722  spanunsni  24917  h1datomi  24919  spansncvi  24990  pjss2i  25018  pjssmii  25019  pjocini  25036  homulid2  25139  honegdi  25148  ho2times  25158  nmopge0  25250  nmopgt0  25251  nmfnge0  25266  lnopaddi  25310  lnopmuli  25311  lnopsubi  25313  hmopbdoptHIL  25327  nmbdoplbi  25363  nmcoplbi  25367  nmophmi  25370  lnopconi  25373  lnfnaddi  25382  lnfnsubi  25385  nmbdfnlbi  25388  nmcfnlbi  25391  lnfnconi  25394  imaelshi  25397  cnlnadjlem2  25407  cnlnadjlem7  25412  nmoptrii  25433  nmopcoi  25434  adjcoi  25439  nmopcoadji  25440  bracnlnval  25453  leopmul  25473  opsqrlem1  25479  opsqrlem6  25484  hmopidmpji  25491  sto2i  25576  strlem1  25589  atcveq0  25687  atcv0eq  25718  atomli  25721  atcvati  25725  atcvat3i  25735  cdjreui  25771  cdj1i  25772  xdiv0  26037  xdivpnfrp  26041  mhmhmeotmd  26293  rezh  26336  qqhucn  26357  blscon  27063  cnllyscon  27064  ghomgrpilem2  27234  ghomsn  27236  sinccvglem  27246  fallrisefac  27457  wfrlem12  27664  frrlem11  27709  nobndlem8  27769  bpoly3  28130  fsumcube  28132  opnmbllem0  28352  mblfinlem3  28355  mblfinlem4  28356  ismblfin  28357  voliunnfl  28360  ftc1anclem5  28396  ftc1anclem6  28397  ftc1anclem7  28398  ftc1anclem8  28399  ftc1anc  28400  opnrebl2  28441  heiborlem7  28641  rrnequiv  28659  ismrer1  28662  mapco2  28976  mzpaddmpt  29002  mzpmulmpt  29003  zindbi  29212  mpaaeu  29432  iswlkg  30210  0vgrargra  30475  zringsubgval  30740  eel000cT  31261  eel0TT  31262  eel011  31265  eel012  31267  cnaddcom  32339
  Copyright terms: Public domain W3C validator