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

Theorem mp3an 1364
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 1351 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 678 1  |-  th
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  vtocl3  3103  raltp  4027  rextp  4028  funopg  5614  ftp  6075  caovass  6469  caovdi  6488  ordom  6701  ofmres  6789  omopthlem1  7356  omopthlem2  7357  omopthi  7358  xpcomen  7663  unfilem3  7837  hartogs  8059  card2on  8069  unwf  8281  tskwe  8384  alephsmo  8533  dfac4  8553  dfac2a  8560  ackbij1lem5  8654  ackbij1lem13  8662  axdc2lem  8878  axcclem  8887  ondomon  8988  cfpwsdom  9009  pwfseqlem2  9084  pwfseqlem3  9085  1lt2pi  9330  addassi  9651  mulassi  9652  adddii  9653  adddiri  9654  lttri  9760  lelttri  9761  ltletri  9762  letri  9763  ltadd2i  9765  ltadd2iOLD  9766  mul02lem2  9810  addid1  9813  addcani  9826  addcan2i  9827  mul12i  9828  mul32i  9829  add12i  9851  add32i  9852  subaddi  9962  subadd2i  9963  subsub23i  9965  addsubassi  9966  addsubi  9967  subcani  9968  subcan2i  9969  pnncani  9970  subdii  10067  subdiri  10068  ltadd1i  10168  leadd1i  10169  leadd2i  10170  ltsubaddi  10171  lesubaddi  10172  ltsubadd2i  10173  lesubadd2i  10174  ltaddsubi  10175  mulcani  10251  div23i  10365  div11i  10366  1mhlfehlf  10832  halfpm6th  10834  addex  11300  mulex  11301  unirnioo  11734  ioorebas  11736  uzenom  12178  nnenom  12193  m1expcl2  12294  i4  12377  expnass  12380  faclbnd4lem1  12478  bcn1  12498  ccatfnOLD  12718  cats1fvn  12954  cats1fv  12955  cats1cat  12957  abs3difi  13471  0.999...  13937  geoihalfsum  13938  bpoly3  14111  ef01bndlem  14238  cos1bnd  14241  cos2bnd  14242  sin4lt0  14249  rpnnen2lem3  14269  rpnnen2lem11  14277  rpnnen  14279  rexpen  14280  aleph1irr  14298  divalglem2  14373  divalglem2OLD  14374  ndvdsi  14391  gcdaddmlem  14492  bezout  14510  3lcm2e6woprm  14580  6lcm4e12  14581  lcmf0  14607  lcmf2a3a4e12  14620  3prm  14641  dec2dvds  15035  modxai  15040  modsubi  15044  gcdi  15045  numexp2x  15051  prdsval  15353  prdsds  15362  mreexexd  15554  plusffval  16493  pmtrprfval  17128  m1expaddsub  17139  0frgp  17429  staffval  18075  scaffval  18109  cnfldcj  18977  cnfldds  18980  xrsadd  18985  xrsmul  18986  xrsds  19011  nn0srg  19037  rge0srg  19038  zring0  19049  cnmsgnsubg  19145  psgninv  19150  re0g  19180  ipffval  19215  ocvfval  19229  frlmbas  19318  mdetrlin  19627  mdetunilem9  19645  leordtval2  20228  iscnp2  20255  utop3cls  21266  nmfval  21603  nmoffn  21716  nmofval  21719  nmoffnOLD  21737  nmofvalOLD  21738  icccld  21787  addcnlem  21896  iimulcn  21966  icopnfhmeo  21971  iccpnfcnv  21972  iccpnfhmeo  21973  xrhmeo  21974  xrhmph  21975  oprpiece1res1  21979  oprpiece1res2  21980  ishtpy  22003  pcoass  22055  tchex  22191  cnfldcusp  22324  resscdrg  22325  reust  22340  recusp  22341  vitalilem4  22569  vitalilem5  22570  mbfdm  22584  dveflem  22931  dvlipcn  22946  c1lip2  22950  dgrid  23218  iaa  23281  abelthlem3  23388  abelthlem5  23390  abelth  23396  efcn  23398  sinhalfpilem  23418  sincosq1lem  23452  sincosq4sgn  23456  tangtx  23460  sincos4thpi  23468  sincos6thpi  23470  pige3  23472  relogcn  23583  dvlog2lem  23597  dvlog2  23598  logtayl  23605  logtayl2  23607  cxpsqrtlem  23647  cxpsqrt  23648  cxpcn2  23686  cxpcn3  23688  logblog  23729  ang180lem1  23738  ang180lem2  23739  1cubrlem  23767  mcubic  23773  quart1lem  23781  quart1  23782  reasinsin  23822  atancj  23836  efiatan  23838  atantan  23849  atanbndlem  23851  atan1  23854  atancn  23862  atantayl2  23864  log2cnv  23870  log2tlbnd  23871  log2ublem1  23872  log2ublem2  23873  log2ub  23875  efrlim  23895  scvxcvx  23911  1sgm2ppw  24128  ppiub  24132  bclbnd  24208  bposlem8  24219  lgsdir2lem1  24251  lgsdir2lem5  24255  lgseisenlem1  24277  lgseisenlem2  24278  lgsquadlem1  24282  chebbnd1  24310  dchrvmasumlem2  24336  istrkg3ld  24509  trgcgrg  24560  ax5seglem7  24965  axlowdimlem6  24977  axlowdimlem8  24979  axlowdimlem11  24982  cusgrasizeindb1  25199  3v3e3cycl1  25372  constr3lem2  25374  constr3lem5  25376  constr3trllem5  25382  erclwwlktr  25543  erclwwlkntr  25555  0egra0rgra  25664  vdegp1ai  25712  usg2spot2nb  25793  ex-fl  25897  0vfval  26225  smcnlem  26333  lnocoi  26398  nmlno0lem  26434  nmblolbii  26440  blocnilem  26445  blocni  26446  cncph  26460  isph  26463  ip0i  26466  ip1ilem  26467  ip2i  26469  ipdirilem  26470  ipasslem7  26477  ipasslem8  26478  ipasslem9  26479  ipasslem10  26480  ipasslem11  26481  ip2dii  26485  pythi  26491  siilem1  26492  siilem2  26493  siii  26494  hvmulassi  26699  hvmulcomi  26700  hvdistr1i  26704  hvsubdistr1i  26705  hvassi  26706  hvadd32i  26707  hvsubassi  26708  hvsub32i  26709  normlem0  26762  normlem8  26770  normlem9  26771  bcseqi  26773  polid2i  26810  hhph  26831  hlim0  26888  shscli  26970  shlessi  27030  shlej1i  27031  omlsilem  27055  shlubi  27068  h1de2i  27206  pjadjii  27327  pjaddii  27328  pjmulii  27330  pjdifnormii  27336  pjcji  27337  hoaddsubassi  27473  eigrei  27487  eigposi  27489  eigorthi  27490  adj0  27647  lnopeq0lem1  27658  lnopunilem1  27663  lnophmlem2  27670  nmcexi  27679  nmcopexi  27680  lnfn0i  27695  nmcfnexi  27704  mdexchi  27988  xppreima2  28249  elxrge02  28401  xrge0adddir  28455  xrnarchi  28501  xrge0slmod  28607  psgnid  28610  raddcn  28735  xrge0iifcnv  28739  xrge0iifiso  28741  xrge0iifhmeo  28742  xrge0iifhom  28743  xrge0iifmhm  28745  xrge0mulc1cn  28747  lmlimxrge0  28754  pnfneige0  28757  lmxrge0  28758  zringnm  28764  rezh  28775  qqh0  28788  qqh1  28789  qqhucn  28796  esumpinfval  28894  hashf2  28905  esumcvg  28907  br2base  29091  sxbrsigalem3  29094  dya2iocbrsiga  29097  dya2icobrsiga  29098  sxbrsigalem1  29107  sxbrsigalem2  29108  sxbrsigalem4  29109  sxbrsigalem5  29110  sxbrsiga  29112  oms0OLD  29129  ballotlem2  29321  ballotlem4  29331  ballotlemi1  29335  ballotth  29370  ballotlemi1OLD  29373  ballotthOLD  29408  sgnclre  29410  signstf  29455  subfacp1lem1  29902  subfacp1lem6  29908  kur14lem6  29934  cvmliftlem4  30011  problem4  30300  quad3  30302  logi  30370  iexpire  30371  fununiq  30410  fvtransport  30799  bj-minftyccb  31667  taupilem2  31723  1oequni2o  31771  finxp1o  31784  finxpreclem4  31786  cos2h  31936  tan2h  31937  pigt3  31938  poimirlem9  31949  poimirlem25  31965  poimirlem27  31967  poimirlem28  31968  ismblfin  31981  mbfposadd  31988  ftc1anclem5  32021  asindmre  32027  dvasin  32028  dvacos  32029  rrnval  32159  dihjatcclem4  34989  rabren3dioph  35658  jm2.27dlem2  35865  rmydioph  35869  rmxdioph  35871  expdiophlem2  35877  expdioph  35878  arearect  36100  areaquad  36101  corclrcl  36299  iunrelexpuztr  36311  corcltrcl  36331  dffrege76  36535  lhe4.4ex1a  36678  binomcxplemdvbinom  36702  binomcxplemnotnn0  36705  ax6e2ndeqALT  37328  sineq0ALT  37334  pnfel0pnf  37629  lptioo2cn  37726  icccncfext  37765  itgsin0pilem1  37826  itgsbtaddcnst  37859  stoweidlem13  37873  wallispilem2  37928  wallispilem4  37930  wallispi2lem1  37933  stirlinglem13  37948  dirkerper  37958  dirkertrigeqlem3  37962  dirkeritg  37964  dirkercncflem1  37965  dirkercncflem4  37968  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem62  38032  fourierdlem102  38072  fourierdlem103  38073  fourierdlem104  38074  fourierdlem114  38084  sqwvfoura  38092  fourierswlem  38094  fouriersw  38095  6gbe  38872  7gbo  38873  8gbe  38874  9gboa  38875  11gboa  38876  sgoldbalt  38882  nnsum4primesevenALTV  38896  3exp4mod41  38916  41prothprmlem2  38918  xnn0xrge0  39076  cusgrsizeindb1  39511  0grrusgr  39595  1wlkntrl  39715  0nodd  39863  oddinmgm  39868  2zrng0  39991  zlmodzxz0  40190  zlmodzxzequa  40342  zlmodzxzequap  40345  zlmodzxzldeplem3  40348  3halfnz  40370  nnlog2ge0lt1  40430  blen1  40448  blen2  40449  nnolog2flm1  40454
  Copyright terms: Public domain W3C validator