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

Theorem mp3an 1324
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 1311 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 672 1  |-  th
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 975
This theorem is referenced by:  vtocl3  3163  raltp  4087  rextp  4088  funopg  5626  ftp  6083  caovass  6474  caovdi  6493  ordom  6708  ofmres  6795  omopthlem1  7322  omopthlem2  7323  omopthi  7324  xpcomen  7627  unfilem3  7804  hartogs  7987  card2on  7998  unwf  8245  tskwe  8348  alephsmo  8500  dfac4  8520  dfac2a  8527  ackbij1lem5  8621  ackbij1lem13  8629  axdc2lem  8845  axcclem  8854  ondomon  8955  cfpwsdom  8976  pwfseqlem2  9054  pwfseqlem3  9055  1lt2pi  9300  addassi  9621  mulassi  9622  adddii  9623  adddiri  9624  lttri  9727  lelttri  9728  ltletri  9729  letri  9730  ltadd2i  9732  ltadd2iOLD  9733  mul02lem2  9774  addid1  9777  addcani  9790  addcan2i  9791  mul12i  9792  mul32i  9793  add12i  9815  add32i  9816  subaddi  9926  subadd2i  9927  subsub23i  9929  addsubassi  9930  addsubi  9931  subcani  9932  subcan2i  9933  pnncani  9934  subdii  10026  subdiri  10027  ltadd1i  10128  leadd1i  10129  leadd2i  10130  ltsubaddi  10131  lesubaddi  10132  ltsubadd2i  10133  lesubadd2i  10134  ltaddsubi  10135  mulcani  10209  div23i  10323  div11i  10324  1mhlfehlf  10779  halfpm6th  10781  addex  11243  mulex  11244  unirnioo  11649  ioorebas  11651  uzenom  12078  nnenom  12093  m1expcl2  12191  i4  12273  expnass  12276  faclbnd4lem1  12374  bcn1  12394  ccatfnOLD  12600  cats1fvn  12835  cats1fv  12836  cats1cat  12838  abs3difi  13253  0.999...  13702  geoihalfsum  13703  ef01bndlem  13931  cos1bnd  13934  cos2bnd  13935  sin4lt0  13942  rpnnen2lem3  13962  rpnnen2lem11  13970  rpnnen  13972  rexpen  13973  aleph1irr  13991  divalglem2  14065  ndvdsi  14080  gcdaddmlem  14178  bezout  14192  3prm  14246  dec2dvds  14561  modxai  14566  modsubi  14570  gcdi  14571  numexp2x  14577  prdsval  14872  prdsds  14881  mreexexd  15065  plusffval  16004  pmtrprfval  16639  m1expaddsub  16650  0frgp  16924  staffval  17623  scaffval  17657  cnfldcj  18554  cnfldds  18557  xrsadd  18562  xrsmul  18563  xrsds  18588  nn0srg  18613  rge0srg  18614  zring0  18625  zrng0  18632  cnmsgnsubg  18740  psgninv  18745  re0g  18775  ipffval  18810  ocvfval  18824  frlmbas  18913  frlmbasOLD  18914  mdetrlin  19231  mdetunilem9  19249  leordtval2  19840  iscnp2  19867  utop3cls  20880  nmfval  21235  nmoffn  21344  nmofval  21347  icccld  21400  addcnlem  21494  iimulcn  21564  icopnfhmeo  21569  iccpnfcnv  21570  iccpnfhmeo  21571  xrhmeo  21572  xrhmph  21573  oprpiece1res1  21577  oprpiece1res2  21578  ishtpy  21598  pcoass  21650  tchex  21786  cnfldcusp  21923  resscdrg  21924  reust  21939  recusp  21940  vitalilem4  22146  vitalilem5  22147  mbfdm  22161  dveflem  22506  dvlipcn  22521  c1lip2  22525  dgrid  22787  iaa  22847  abelthlem3  22954  abelthlem5  22956  abelth  22962  efcn  22964  sinhalfpilem  22982  sincosq1lem  23016  sincosq4sgn  23020  tangtx  23024  sincos4thpi  23032  sincos6thpi  23034  pige3  23036  relogcn  23145  dvlog2lem  23159  dvlog2  23160  logtayl  23167  logtayl2  23169  cxpsqrtlem  23209  cxpsqrt  23210  cxpcn2  23246  cxpcn3  23248  ang180lem1  23267  ang180lem2  23268  1cubrlem  23298  mcubic  23304  quart1lem  23312  quart1  23313  reasinsin  23353  atancj  23367  efiatan  23369  atantan  23380  atanbndlem  23382  atan1  23385  atancn  23393  atantayl2  23395  log2cnv  23401  log2tlbnd  23402  log2ublem1  23403  log2ublem2  23404  log2ub  23406  efrlim  23425  scvxcvx  23441  1sgm2ppw  23601  ppiub  23605  bclbnd  23681  bposlem8  23692  lgsdir2lem1  23724  lgsdir2lem5  23728  lgseisenlem1  23750  lgseisenlem2  23751  lgsquadlem1  23755  chebbnd1  23783  dchrvmasumlem2  23809  trgcgrg  24032  ax5seglem7  24365  axlowdimlem6  24377  axlowdimlem8  24379  axlowdimlem11  24382  cusgrasizeindb1  24598  3v3e3cycl1  24771  constr3lem2  24773  constr3lem5  24775  constr3trllem5  24781  erclwwlktr  24942  erclwwlkntr  24954  0egra0rgra  25063  vdegp1ai  25111  usg2spot2nb  25192  ex-fl  25295  0vfval  25626  smcnlem  25734  lnocoi  25799  nmlno0lem  25835  nmblolbii  25841  blocnilem  25846  blocni  25847  cncph  25861  isph  25864  ip0i  25867  ip1ilem  25868  ip2i  25870  ipdirilem  25871  ipasslem7  25878  ipasslem8  25879  ipasslem9  25880  ipasslem10  25881  ipasslem11  25882  ip2dii  25886  pythi  25892  siilem1  25893  siilem2  25894  siii  25895  hvmulassi  26090  hvmulcomi  26091  hvdistr1i  26095  hvsubdistr1i  26096  hvassi  26097  hvadd32i  26098  hvsubassi  26099  hvsub32i  26100  normlem0  26153  normlem8  26161  normlem9  26162  bcseqi  26164  polid2i  26201  hhph  26222  hlim0  26280  shscli  26362  shlessi  26422  shlej1i  26423  omlsilem  26447  shlubi  26460  h1de2i  26598  pjadjii  26719  pjaddii  26720  pjmulii  26722  pjdifnormii  26728  pjcji  26729  hoaddsubassi  26866  eigrei  26880  eigposi  26882  eigorthi  26883  adj0  27040  lnopeq0lem1  27051  lnopunilem1  27056  lnophmlem2  27063  nmcexi  27072  nmcopexi  27073  lnfn0i  27088  nmcfnexi  27097  mdexchi  27381  xppreima2  27636  elxrge02  27788  xrge0adddir  27842  xrnarchi  27888  xrge0slmod  27995  raddcn  28072  xrge0iifcnv  28076  xrge0iifiso  28078  xrge0iifhmeo  28079  xrge0iifhom  28080  xrge0iifmhm  28082  xrge0mulc1cn  28084  lmlimxrge0  28091  pnfneige0  28094  lmxrge0  28095  zringnm  28101  zzsnmOLD  28103  rezh  28113  qqh0  28126  qqh1  28127  qqhucn  28134  esumpinfval  28245  hashf2  28256  esumcvg  28258  br2base  28413  sxbrsigalem3  28416  dya2iocbrsiga  28419  dya2icobrsiga  28420  sxbrsigalem1  28429  sxbrsigalem2  28430  sxbrsigalem4  28431  sxbrsigalem5  28432  sxbrsiga  28434  oms0  28441  ballotlem2  28624  ballotlem4  28634  ballotlemi1  28638  ballotth  28673  sgnclre  28675  signstf  28720  subfacp1lem1  28820  subfacp1lem6  28826  kur14lem6  28852  cvmliftlem4  28930  problem4  29219  quad3  29221  logi  29339  iexpire  29340  fununiq  29417  fvtransport  29887  bpoly3  30025  cos2h  30251  tan2h  30252  ismblfin  30260  mbfposadd  30267  ftc1anclem5  30299  asindmre  30307  dvasin  30308  dvacos  30309  rrnval  30528  rabren3dioph  30953  jm2.27dlem2  31156  rmydioph  31160  rmxdioph  31162  expdiophlem2  31168  expdioph  31169  arearect  31387  areaquad  31388  lhe4.4ex1a  31438  binomcxplemdvbinom  31462  binomcxplemnotnn0  31465  lptioo2cn  31854  icccncfext  31893  itgsin0pilem1  31951  itgsbtaddcnst  31984  stoweidlem13  31998  wallispilem2  32051  wallispilem4  32053  wallispi2lem1  32056  stirlinglem13  32071  dirkerper  32081  dirkertrigeqlem3  32085  dirkeritg  32087  dirkercncflem1  32088  dirkercncflem4  32091  fourierdlem42  32134  fourierdlem62  32154  fourierdlem102  32194  fourierdlem103  32195  fourierdlem104  32196  fourierdlem114  32206  sqwvfoura  32214  fourierswlem  32216  fouriersw  32217  0nodd  32760  oddinmgm  32765  2zrng0  32888  zlmodzxz0  33089  zlmodzxzequa  33241  zlmodzxzequap  33244  zlmodzxzldeplem3  33247  ax6e2ndeqALT  33874  sineq0ALT  33880  bj-minftyccb  34771  dihjatcclem4  37291  taupilem2  37840
  Copyright terms: Public domain W3C validator