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

Theorem mp3an1 1267
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 1155 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 653 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  mp3an12  1270  mp3an1i  1273  mp3anl1  1274  mp3an  1280  onint  4777  tfrlem9  6648  oaord1  6796  oaword2  6798  oawordeulem  6799  oa00  6804  omword1  6818  omword2  6819  omlimcl  6823  oeoelem  6843  nnaordex  6883  enp1i  7345  unfilem2  7374  dffi3  7438  unbnn3  7615  pwcdaen  8067  ackbij1b  8121  zorn2  8388  zornn0  8390  ttukey  8400  brdom7disj  8411  brdom6disj  8412  wunex2  8615  muladd11  9238  00id  9243  mul02  9246  negsubdi  9359  mulneg1  9472  ltaddpos  9520  addge01  9540  reccl  9687  recid  9694  recid2  9695  recdiv2  9729  divdiv23zi  9769  ltmul12a  9868  lemul12a  9870  mulgt1  9871  ltmulgt11  9872  gt0div  9878  ge0div  9879  lediv12a  9905  ledivp1  9914  ltdiv23i  9937  ledivp1i  9938  ltdivp1i  9939  infm3  9969  infmrcl  9989  nngt1ne1  10029  8th4div3  10193  gtndiv  10349  nn0ind  10368  fnn0ind  10371  supminf  10565  xrre2  10760  qsqueeze  10789  xmulpnf1  10855  xlemul1a  10869  xrub  10892  ioorebas  11008  expubnd  11442  le2sq2  11459  crreczi  11506  bernneq  11507  faclbnd5  11591  faclbnd6  11592  bccl  11615  hashbc  11704  ccatlid  11750  shftfval  11887  mulre  11928  sqrlem4  12053  sqrlem7  12056  sqreulem  12165  binom1p  12612  0.999...  12660  efsub  12703  efi4p  12740  sinadd  12767  cosadd  12768  cos2t  12781  cos2tsin  12782  sin01gt0  12793  cos01gt0  12794  absefib  12801  efieq1re  12802  demoivreALT  12804  rpnnen2lem4  12819  odd2np1  12910  divalglem0  12915  divalglem4  12918  divalglem9  12923  gcdcllem3  13015  gcdn0gt0  13024  gcdadd  13032  gcdmultiple  13052  algcvgblem  13070  algcvga  13072  isprm3  13090  coprm  13102  divgcdodd  13121  phibndlem  13161  opoe  13187  omoe  13188  opeo  13189  omeo  13190  pythagtriplem4  13195  pythagtriplem11  13201  pythagtriplem12  13202  pythagtriplem13  13203  pythagtriplem14  13204  infpn2  13283  1arith2  13298  vdwap0  13346  vdwap1  13347  ipolt  14587  gsumval2a  14784  mplsubrglem  16504  cnfldneg  16729  cnflddiv  16733  cnfldmulg  16735  cnfldexp  16736  thlleval  16927  neiptoptop  17197  iccordt  17280  divstgplem  18152  bl2ioo  18825  ioo2blex  18827  blssioo  18828  tgioo  18829  xrsblre  18844  iccntr  18854  icccmplem3  18857  reconnlem2  18860  opnreen  18864  iccpnfcnv  18971  cnllycmp  18983  pcoptcl  19048  ovolmge0  19375  ovolctb2  19390  ismbl2  19425  cmmbl  19431  nulmbl  19432  unmbl  19434  voliunlem1  19446  voliunlem2  19447  ioombl1  19458  opnmbllem  19495  mbfima  19526  i1fsub  19602  itg1sub  19603  ellimc3  19768  limcflf  19770  dvcnvre  19905  coe1termlem  20178  dgrsub  20192  dvnply2  20206  dvnply  20207  reeff1o  20365  sinperlem  20390  sincosq1eq  20422  resinf1o  20440  logeftb  20480  logge0  20502  logdivlti  20517  efopn  20551  logtayl2  20555  loglesqr  20644  logrec  20663  xrlimcnp  20809  ppinncl  20959  chtrpcl  20960  bposlem2  21071  bposlem8  21077  lgsdir2  21114  1lgs  21123  redwlklem  21607  isgrpoi  21788  grpo2grp  21824  imsmetlem  22184  nmcvcn  22193  ipval2  22205  lnocoi  22260  nmlno0lem  22296  nmblolbii  22302  blometi  22306  blocnilem  22307  blocni  22308  ipasslem1  22334  ipasslem2  22335  ipasslem4  22337  ipasslem5  22338  ipasslem8  22340  ipblnfi  22359  ip2eqi  22360  ubthlem1  22374  htthlem  22422  h2hmetdval  22483  axhvcom-zf  22488  axhis1-zf  22499  axhis4-zf  22502  hvm1neg  22536  hvsub4  22541  hvsubass  22548  hvsubdistr2  22554  hv2times  22565  hvsubcan  22578  hvsubcan2  22579  his2sub  22596  norm-i  22633  normpyc  22650  hhip  22681  hhph  22682  norm1exi  22754  hhssabloi  22764  hhssnv  22766  hhshsslem2  22770  hhssmetdval  22780  shscli  22821  shunssi  22872  shsleji  22874  shsidmi  22888  spanunsni  23083  h1datomi  23085  spansncvi  23156  pjss2i  23184  pjssmii  23185  pjocini  23202  homulid2  23305  honegdi  23314  ho2times  23324  nmopge0  23416  nmopgt0  23417  nmfnge0  23432  lnopaddi  23476  lnopmuli  23477  lnopsubi  23479  hmopbdoptHIL  23493  nmbdoplbi  23529  nmcoplbi  23533  nmophmi  23536  lnopconi  23539  lnfnaddi  23548  lnfnsubi  23551  nmbdfnlbi  23554  nmcfnlbi  23557  lnfnconi  23560  imaelshi  23563  cnlnadjlem2  23573  cnlnadjlem7  23578  nmoptrii  23599  nmopcoi  23600  adjcoi  23605  nmopcoadji  23606  bracnlnval  23619  leopmul  23639  opsqrlem1  23645  opsqrlem6  23650  hmopidmpji  23657  sto2i  23742  strlem1  23755  atcveq0  23853  atcv0eq  23884  atomli  23887  atcvati  23891  atcvat3i  23901  cdjreui  23937  cdj1i  23938  xdiv0  24177  xdivpnfrp  24181  zzsmulg  24267  remulg  24272  mhmhmeotmd  24315  rezh  24357  qqhucn  24378  blscon  24933  cnllyscon  24934  ghomgrpilem2  25099  ghomsn  25101  sinccvglem  25111  fallrisefac  25343  wfrlem12  25551  frrlem11  25596  nobndlem8  25656  brbtwn2  25846  colinearalglem4  25850  ax5seglem1  25869  ax5seglem2  25870  axcontlem2  25906  axcontlem4  25908  axcontlem7  25911  bpoly3  26106  fsumcube  26108  opnmbllem0  26244  mblfinlem3  26247  mblfinlem4  26248  ismblfin  26249  voliunnfl  26252  ftc1anclem5  26286  ftc1anclem6  26287  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290  opnrebl2  26326  heiborlem7  26528  rrnequiv  26546  ismrer1  26549  mapco2  26772  mzpaddmpt  26800  mzpmulmpt  26801  zindbi  27011  frlmsslsp  27227  mpaaeu  27334  f1otrspeq  27369  elfzelfzelfz  28111  iswlkg  28302  0vgrargra  28378  sgnp  28522  eel000cT  28808  eel0TT  28809  eel011  28812  eel012  28814  cnaddcom  29771
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator