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

Theorem mp3an 1360
Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
Hypotheses
Ref Expression
mp3an.1  |-  ph
mp3an.2  |-  ps
mp3an.3  |-  ch
mp3an.4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an  |-  th

Proof of Theorem mp3an
StepHypRef Expression
1 mp3an.2 . 2  |-  ps
2 mp3an.3 . 2  |-  ch
3 mp3an.1 . . 3  |-  ph
4 mp3an.4 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
53, 4mp3an1 1347 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 676 1  |-  th
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  vtocl3  3135  raltp  4052  rextp  4053  funopg  5630  ftp  6087  caovass  6480  caovdi  6499  ordom  6712  ofmres  6800  omopthlem1  7361  omopthlem2  7362  omopthi  7363  xpcomen  7666  unfilem3  7840  hartogs  8062  card2on  8072  unwf  8283  tskwe  8386  alephsmo  8534  dfac4  8554  dfac2a  8561  ackbij1lem5  8655  ackbij1lem13  8663  axdc2lem  8879  axcclem  8888  ondomon  8989  cfpwsdom  9010  pwfseqlem2  9085  pwfseqlem3  9086  1lt2pi  9331  addassi  9652  mulassi  9653  adddii  9654  adddiri  9655  lttri  9761  lelttri  9762  ltletri  9763  letri  9764  ltadd2i  9766  ltadd2iOLD  9767  mul02lem2  9811  addid1  9814  addcani  9827  addcan2i  9828  mul12i  9829  mul32i  9830  add12i  9852  add32i  9853  subaddi  9963  subadd2i  9964  subsub23i  9966  addsubassi  9967  addsubi  9968  subcani  9969  subcan2i  9970  pnncani  9971  subdii  10068  subdiri  10069  ltadd1i  10169  leadd1i  10170  leadd2i  10171  ltsubaddi  10172  lesubaddi  10173  ltsubadd2i  10174  lesubadd2i  10175  ltaddsubi  10176  mulcani  10252  div23i  10366  div11i  10367  1mhlfehlf  10833  halfpm6th  10835  addex  11301  mulex  11302  unirnioo  11735  ioorebas  11737  uzenom  12178  nnenom  12193  m1expcl2  12294  i4  12377  expnass  12380  faclbnd4lem1  12478  bcn1  12498  ccatfnOLD  12711  cats1fvn  12945  cats1fv  12946  cats1cat  12948  abs3difi  13460  0.999...  13925  geoihalfsum  13926  bpoly3  14099  ef01bndlem  14226  cos1bnd  14229  cos2bnd  14230  sin4lt0  14237  rpnnen2lem3  14257  rpnnen2lem11  14265  rpnnen  14267  rexpen  14268  aleph1irr  14286  divalglem2  14361  divalglem2OLD  14362  ndvdsi  14379  gcdaddmlem  14480  bezout  14498  3lcm2e6woprm  14568  6lcm4e12  14569  lcmf0  14595  lcmf2a3a4e12  14608  3prm  14629  dec2dvds  15023  modxai  15028  modsubi  15032  gcdi  15033  numexp2x  15039  prdsval  15341  prdsds  15350  mreexexd  15542  plusffval  16481  pmtrprfval  17116  m1expaddsub  17127  0frgp  17417  staffval  18063  scaffval  18097  cnfldcj  18965  cnfldds  18968  xrsadd  18973  xrsmul  18974  xrsds  18999  nn0srg  19024  rge0srg  19025  zring0  19036  cnmsgnsubg  19132  psgninv  19137  re0g  19167  ipffval  19202  ocvfval  19216  frlmbas  19305  mdetrlin  19614  mdetunilem9  19632  leordtval2  20215  iscnp2  20242  utop3cls  21253  nmfval  21590  nmoffn  21703  nmofval  21706  nmoffnOLD  21724  nmofvalOLD  21725  icccld  21774  addcnlem  21883  iimulcn  21953  icopnfhmeo  21958  iccpnfcnv  21959  iccpnfhmeo  21960  xrhmeo  21961  xrhmph  21962  oprpiece1res1  21966  oprpiece1res2  21967  ishtpy  21990  pcoass  22042  tchex  22178  cnfldcusp  22311  resscdrg  22312  reust  22327  recusp  22328  vitalilem4  22556  vitalilem5  22557  mbfdm  22571  dveflem  22918  dvlipcn  22933  c1lip2  22937  dgrid  23205  iaa  23268  abelthlem3  23375  abelthlem5  23377  abelth  23383  efcn  23385  sinhalfpilem  23405  sincosq1lem  23439  sincosq4sgn  23443  tangtx  23447  sincos4thpi  23455  sincos6thpi  23457  pige3  23459  relogcn  23570  dvlog2lem  23584  dvlog2  23585  logtayl  23592  logtayl2  23594  cxpsqrtlem  23634  cxpsqrt  23635  cxpcn2  23673  cxpcn3  23675  logblog  23716  ang180lem1  23725  ang180lem2  23726  1cubrlem  23754  mcubic  23760  quart1lem  23768  quart1  23769  reasinsin  23809  atancj  23823  efiatan  23825  atantan  23836  atanbndlem  23838  atan1  23841  atancn  23849  atantayl2  23851  log2cnv  23857  log2tlbnd  23858  log2ublem1  23859  log2ublem2  23860  log2ub  23862  efrlim  23882  scvxcvx  23898  1sgm2ppw  24115  ppiub  24119  bclbnd  24195  bposlem8  24206  lgsdir2lem1  24238  lgsdir2lem5  24242  lgseisenlem1  24264  lgseisenlem2  24265  lgsquadlem1  24269  chebbnd1  24297  dchrvmasumlem2  24323  istrkg3ld  24496  trgcgrg  24547  ax5seglem7  24952  axlowdimlem6  24964  axlowdimlem8  24966  axlowdimlem11  24969  cusgrasizeindb1  25185  3v3e3cycl1  25358  constr3lem2  25360  constr3lem5  25362  constr3trllem5  25368  erclwwlktr  25529  erclwwlkntr  25541  0egra0rgra  25650  vdegp1ai  25698  usg2spot2nb  25779  ex-fl  25883  0vfval  26211  smcnlem  26319  lnocoi  26384  nmlno0lem  26420  nmblolbii  26426  blocnilem  26431  blocni  26432  cncph  26446  isph  26449  ip0i  26452  ip1ilem  26453  ip2i  26455  ipdirilem  26456  ipasslem7  26463  ipasslem8  26464  ipasslem9  26465  ipasslem10  26466  ipasslem11  26467  ip2dii  26471  pythi  26477  siilem1  26478  siilem2  26479  siii  26480  hvmulassi  26685  hvmulcomi  26686  hvdistr1i  26690  hvsubdistr1i  26691  hvassi  26692  hvadd32i  26693  hvsubassi  26694  hvsub32i  26695  normlem0  26748  normlem8  26756  normlem9  26757  bcseqi  26759  polid2i  26796  hhph  26817  hlim0  26874  shscli  26956  shlessi  27016  shlej1i  27017  omlsilem  27041  shlubi  27054  h1de2i  27192  pjadjii  27313  pjaddii  27314  pjmulii  27316  pjdifnormii  27322  pjcji  27323  hoaddsubassi  27459  eigrei  27473  eigposi  27475  eigorthi  27476  adj0  27633  lnopeq0lem1  27644  lnopunilem1  27649  lnophmlem2  27656  nmcexi  27665  nmcopexi  27666  lnfn0i  27681  nmcfnexi  27690  mdexchi  27974  xppreima2  28239  elxrge02  28396  xrge0adddir  28450  xrnarchi  28496  xrge0slmod  28603  psgnid  28606  raddcn  28731  xrge0iifcnv  28735  xrge0iifiso  28737  xrge0iifhmeo  28738  xrge0iifhom  28739  xrge0iifmhm  28741  xrge0mulc1cn  28743  lmlimxrge0  28750  pnfneige0  28753  lmxrge0  28754  zringnm  28760  rezh  28771  qqh0  28784  qqh1  28785  qqhucn  28792  esumpinfval  28890  hashf2  28901  esumcvg  28903  br2base  29087  sxbrsigalem3  29090  dya2iocbrsiga  29093  dya2icobrsiga  29094  sxbrsigalem1  29103  sxbrsigalem2  29104  sxbrsigalem4  29105  sxbrsigalem5  29106  sxbrsiga  29108  oms0OLD  29125  ballotlem2  29317  ballotlem4  29327  ballotlemi1  29331  ballotth  29366  ballotlemi1OLD  29369  ballotthOLD  29404  sgnclre  29406  signstf  29451  subfacp1lem1  29898  subfacp1lem6  29904  kur14lem6  29930  cvmliftlem4  30007  problem4  30296  quad3  30298  logi  30365  iexpire  30366  fununiq  30405  fvtransport  30792  bj-minftyccb  31619  taupilem2  31675  cos2h  31850  tan2h  31851  pigt3  31852  poimirlem9  31863  poimirlem25  31879  poimirlem27  31881  poimirlem28  31882  ismblfin  31895  mbfposadd  31902  ftc1anclem5  31935  asindmre  31941  dvasin  31942  dvacos  31943  rrnval  32073  dihjatcclem4  34908  rabren3dioph  35577  jm2.27dlem2  35785  rmydioph  35789  rmxdioph  35791  expdiophlem2  35797  expdioph  35798  arearect  36020  areaquad  36021  corclrcl  36159  iunrelexpuztr  36171  corcltrcl  36191  dffrege76  36393  lhe4.4ex1a  36536  binomcxplemdvbinom  36560  binomcxplemnotnn0  36563  ax6e2ndeqALT  37189  sineq0ALT  37195  pnfel0pnf  37460  lptioo2cn  37546  icccncfext  37585  itgsin0pilem1  37646  itgsbtaddcnst  37679  stoweidlem13  37693  wallispilem2  37748  wallispilem4  37750  wallispi2lem1  37753  stirlinglem13  37768  dirkerper  37778  dirkertrigeqlem3  37782  dirkeritg  37784  dirkercncflem1  37785  dirkercncflem4  37788  fourierdlem42  37832  fourierdlem42OLD  37833  fourierdlem62  37852  fourierdlem102  37892  fourierdlem103  37893  fourierdlem104  37894  fourierdlem114  37904  sqwvfoura  37912  fourierswlem  37914  fouriersw  37915  6gbe  38584  7gbo  38585  8gbe  38586  9gboa  38587  11gboa  38588  sgoldbalt  38594  nnsum4primesevenALTV  38608  3exp4mod41  38628  41prothprmlem2  38630  0nodd  39082  oddinmgm  39087  2zrng0  39210  zlmodzxz0  39411  zlmodzxzequa  39563  zlmodzxzequap  39566  zlmodzxzldeplem3  39569  3halfnz  39591  nnlog2ge0lt1  39651  blen1  39669  blen2  39670  nnolog2flm1  39675
  Copyright terms: Public domain W3C validator