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

Theorem mp3an 1390
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 1377 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 686 1  |-  th
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  vtocl3  3089  raltp  4018  rextp  4019  funopg  5621  feq12i  5732  ftp  6091  caovass  6488  caovdi  6507  ordom  6720  ofmres  6808  omopthlem1  7374  omopthlem2  7375  omopthi  7376  xpcomen  7681  unfilem3  7855  hartogs  8077  card2on  8087  unwf  8299  tskwe  8402  alephsmo  8551  dfac4  8571  dfac2a  8578  ackbij1lem5  8672  ackbij1lem13  8680  axdc2lem  8896  axcclem  8905  ondomon  9006  cfpwsdom  9027  pwfseqlem2  9102  pwfseqlem3  9103  1lt2pi  9348  addassi  9669  mulassi  9670  adddii  9671  adddiri  9672  lttri  9778  lelttri  9779  ltletri  9780  letri  9781  ltadd2i  9783  mul02lem2  9828  addid1  9831  addcani  9844  addcan2i  9845  mul12i  9846  mul32i  9847  add12i  9872  add32i  9873  subaddi  9981  subadd2i  9982  subsub23i  9984  addsubassi  9985  addsubi  9986  subcani  9987  subcan2i  9988  pnncani  9989  subdii  10088  subdiri  10089  ltadd1i  10189  leadd1i  10190  leadd2i  10191  ltsubaddi  10192  lesubaddi  10193  ltsubadd2i  10194  lesubadd2i  10195  ltaddsubi  10196  mulcani  10273  div23i  10387  div11i  10388  1mhlfehlf  10855  halfpm6th  10857  addex  11323  mulex  11324  unirnioo  11759  ioorebas  11761  uzenom  12216  nnenom  12231  m1expcl2  12332  i4  12415  expnass  12418  faclbnd4lem1  12516  bcn1  12536  ccatfnOLD  12769  cats1fvn  13013  cats1fv  13014  cats1cat  13016  cats2cat  13017  wrdlen3s3  13099  abs3difi  13548  0.999...  14014  geoihalfsum  14015  bpoly3  14188  ef01bndlem  14315  cos1bnd  14318  cos2bnd  14319  sin4lt0  14326  rpnnen2lem3  14346  rpnnen2lem11  14354  rpnnen  14356  rexpen  14357  aleph1irr  14375  divalglem2  14452  divalglem2OLD  14453  ndvdsi  14470  gcdaddmlem  14571  bezout  14589  3lcm2e6woprm  14659  6lcm4e12  14660  lcmf0  14686  lcmf2a3a4e12  14699  3prm  14720  dec2dvds  15114  modxai  15119  modsubi  15123  gcdi  15124  numexp2x  15130  prdsval  15431  prdsds  15440  mreexexd  15632  plusffval  16571  pmtrprfval  17206  m1expaddsub  17217  0frgp  17507  staffval  18153  scaffval  18187  cnfldcj  19054  cnfldds  19057  xrsadd  19062  xrsmul  19063  xrsds  19088  nn0srg  19114  rge0srg  19115  zring0  19126  cnmsgnsubg  19222  psgninv  19227  re0g  19257  ipffval  19292  ocvfval  19306  frlmbas  19395  mdetrlin  19704  mdetunilem9  19722  leordtval2  20305  iscnp2  20332  utop3cls  21344  nmfval  21681  nmoffn  21794  nmofval  21797  nmoffnOLD  21815  nmofvalOLD  21816  icccld  21865  addcnlem  21974  iimulcn  22044  icopnfhmeo  22049  iccpnfcnv  22050  iccpnfhmeo  22051  xrhmeo  22052  xrhmph  22053  oprpiece1res1  22057  oprpiece1res2  22058  ishtpy  22081  pcoass  22133  tchex  22269  cnfldcusp  22402  resscdrg  22403  reust  22418  recusp  22419  vitalilem4  22648  vitalilem5  22649  mbfdm  22663  dveflem  23010  dvlipcn  23025  c1lip2  23029  dgrid  23297  iaa  23360  abelthlem3  23467  abelthlem5  23469  abelth  23475  efcn  23477  sinhalfpilem  23497  sincosq1lem  23531  sincosq4sgn  23535  tangtx  23539  sincos4thpi  23547  sincos6thpi  23549  pige3  23551  relogcn  23662  dvlog2lem  23676  dvlog2  23677  logtayl  23684  logtayl2  23686  cxpsqrtlem  23726  cxpsqrt  23727  cxpcn2  23765  cxpcn3  23767  logblog  23808  ang180lem1  23817  ang180lem2  23818  1cubrlem  23846  mcubic  23852  quart1lem  23860  quart1  23861  reasinsin  23901  atancj  23915  efiatan  23917  atantan  23928  atanbndlem  23930  atan1  23933  atancn  23941  atantayl2  23943  log2cnv  23949  log2tlbnd  23950  log2ublem1  23951  log2ublem2  23952  log2ub  23954  efrlim  23974  scvxcvx  23990  1sgm2ppw  24207  ppiub  24211  bclbnd  24287  bposlem8  24298  lgsdir2lem1  24330  lgsdir2lem5  24334  lgseisenlem1  24356  lgseisenlem2  24357  lgsquadlem1  24361  chebbnd1  24389  dchrvmasumlem2  24415  istrkg3ld  24588  trgcgrg  24639  ax5seglem7  25044  axlowdimlem6  25056  axlowdimlem8  25058  axlowdimlem11  25061  cusgrasizeindb1  25278  3v3e3cycl1  25451  constr3lem2  25453  constr3lem5  25455  constr3trllem5  25461  erclwwlktr  25622  erclwwlkntr  25634  0egra0rgra  25743  vdegp1ai  25791  usg2spot2nb  25872  ex-fl  25976  0vfval  26306  smcnlem  26414  lnocoi  26479  nmlno0lem  26515  nmblolbii  26521  blocnilem  26526  blocni  26527  cncph  26541  isph  26544  ip0i  26547  ip1ilem  26548  ip2i  26550  ipdirilem  26551  ipasslem7  26558  ipasslem8  26559  ipasslem9  26560  ipasslem10  26561  ipasslem11  26562  ip2dii  26566  pythi  26572  siilem1  26573  siilem2  26574  siii  26575  hvmulassi  26780  hvmulcomi  26781  hvdistr1i  26785  hvsubdistr1i  26786  hvassi  26787  hvadd32i  26788  hvsubassi  26789  hvsub32i  26790  normlem0  26843  normlem8  26851  normlem9  26852  bcseqi  26854  polid2i  26891  hhph  26912  hlim0  26969  shscli  27051  shlessi  27111  shlej1i  27112  omlsilem  27136  shlubi  27149  h1de2i  27287  pjadjii  27408  pjaddii  27409  pjmulii  27411  pjdifnormii  27417  pjcji  27418  hoaddsubassi  27554  eigrei  27568  eigposi  27570  eigorthi  27571  adj0  27728  lnopeq0lem1  27739  lnopunilem1  27744  lnophmlem2  27751  nmcexi  27760  nmcopexi  27761  lnfn0i  27776  nmcfnexi  27785  mdexchi  28069  xppreima2  28325  elxrge02  28476  xrge0adddir  28529  xrnarchi  28575  xrge0slmod  28681  psgnid  28684  raddcn  28809  xrge0iifcnv  28813  xrge0iifiso  28815  xrge0iifhmeo  28816  xrge0iifhom  28817  xrge0iifmhm  28819  xrge0mulc1cn  28821  lmlimxrge0  28828  pnfneige0  28831  lmxrge0  28832  zringnm  28838  rezh  28849  qqh0  28862  qqh1  28863  qqhucn  28870  esumpinfval  28968  hashf2  28979  esumcvg  28981  br2base  29164  sxbrsigalem3  29167  dya2iocbrsiga  29170  dya2icobrsiga  29171  sxbrsigalem1  29180  sxbrsigalem2  29181  sxbrsigalem4  29182  sxbrsigalem5  29183  sxbrsiga  29185  oms0OLD  29202  ballotlem2  29394  ballotlem4  29404  ballotlemi1  29408  ballotth  29443  ballotlemi1OLD  29446  ballotthOLD  29481  sgnclre  29483  signstf  29527  subfacp1lem1  29974  subfacp1lem6  29980  kur14lem6  30006  cvmliftlem4  30083  problem4  30372  quad3  30374  logi  30441  iexpire  30442  fununiq  30481  fvtransport  30870  bj-minftyccb  31737  taupilem2  31793  1oequni2o  31841  finxp1o  31854  finxpreclem4  31856  cos2h  32000  tan2h  32001  pigt3  32002  poimirlem9  32013  poimirlem25  32029  poimirlem27  32031  poimirlem28  32032  ismblfin  32045  mbfposadd  32052  ftc1anclem5  32085  asindmre  32091  dvasin  32092  dvacos  32093  rrnval  32223  dihjatcclem4  35060  rabren3dioph  35729  jm2.27dlem2  35936  rmydioph  35940  rmxdioph  35942  expdiophlem2  35948  expdioph  35949  arearect  36171  areaquad  36172  corclrcl  36370  iunrelexpuztr  36382  corcltrcl  36402  dffrege76  36606  lhe4.4ex1a  36748  binomcxplemdvbinom  36772  binomcxplemnotnn0  36775  ax6e2ndeqALT  37391  sineq0ALT  37397  pnfel0pnf  37725  lptioo2cn  37823  icccncfext  37862  itgsin0pilem1  37923  itgsbtaddcnst  37956  stoweidlem13  37985  wallispilem2  38040  wallispilem4  38042  wallispi2lem1  38045  stirlinglem13  38060  dirkerper  38070  dirkertrigeqlem3  38074  dirkeritg  38076  dirkercncflem1  38077  dirkercncflem4  38080  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem62  38144  fourierdlem102  38184  fourierdlem103  38185  fourierdlem104  38186  fourierdlem114  38196  sqwvfoura  38204  fourierswlem  38206  fouriersw  38207  6gbe  39017  7gbo  39018  8gbe  39019  9gboa  39020  11gboa  39021  sgoldbalt  39027  nnsum4primesevenALTV  39041  3exp4mod41  39061  41prothprmlem2  39063  xnn0xrge0  39226  cusgrsizeindb1  39676  0grrusgr  39784  1wlk2v2e  40045  ntrl2v2e  40046  upgr3v3e3cycl  40094  konigsberglem1  40166  konigsberglem2  40167  konigsberglem3  40168  konigsberglem5  40170  0nodd  40318  oddinmgm  40323  2zrng0  40446  zlmodzxz0  40645  zlmodzxzequa  40797  zlmodzxzequap  40800  zlmodzxzldeplem3  40803  3halfnz  40825  nnlog2ge0lt1  40885  blen1  40903  blen2  40904  nnolog2flm1  40909
  Copyright terms: Public domain W3C validator