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

Theorem mp3an 1279
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 1266 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 654 1  |-  th
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  vtocl3  2968  raltp  3823  rextp  3824  ordom  4813  funopg  5444  ftp  5876  caovass  6206  caovdi  6225  ofmres  6302  omopthlem1  6857  omopthlem2  6858  omopthi  6859  xpcomen  7158  unfilem3  7332  hartogs  7469  card2on  7478  unwf  7692  tskwe  7793  alephsmo  7939  dfac4  7959  dfac2a  7966  ackbij1lem5  8060  ackbij1lem13  8068  axdc2lem  8284  axcclem  8293  ondomon  8394  cfpwsdom  8415  pwfseqlem2  8490  pwfseqlem3  8491  1lt2pi  8738  addassi  9054  mulassi  9055  adddii  9056  adddiri  9057  lttri  9155  lelttri  9156  ltletri  9157  letri  9158  ltadd2i  9160  mul02lem2  9199  addid1  9202  addcani  9215  addcan2i  9216  mul12i  9217  mul32i  9218  add12i  9239  add32i  9240  subaddi  9343  subadd2i  9344  subsub23i  9346  addsubassi  9347  addsubi  9348  subcani  9349  subcan2i  9350  pnncani  9351  subdii  9438  subdiri  9439  ltadd1i  9537  leadd1i  9538  leadd2i  9539  ltsubaddi  9540  lesubaddi  9541  ltsubadd2i  9542  lesubadd2i  9543  ltaddsubi  9544  mulcani  9617  div23i  9728  div11i  9729  1mhlfehlf  10146  halfpm6th  10148  addex  10566  mulex  10567  unirnioo  10960  ioorebas  10962  uzenom  11259  nnenom  11274  m1expcl2  11358  i4  11438  expnass  11441  faclbnd4lem1  11539  bcn1  11559  ccatfn  11696  cats1fvn  11777  cats1fv  11778  cats1cat  11780  abs3difi  12167  0.999...  12613  geoihalfsum  12614  ef01bndlem  12740  cos1bnd  12743  cos2bnd  12744  sin4lt0  12751  rpnnen2lem3  12771  rpnnen2lem11  12779  rpnnen  12781  rexpen  12782  aleph1irr  12800  divalglem2  12870  ndvdsi  12885  gcdaddmlem  12983  bezout  12997  3prm  13051  dec2dvds  13354  modxai  13359  modsubi  13363  gcdi  13364  numexp2x  13370  prdsval  13633  prdsds  13641  mreexexd  13828  plusffval  14657  0frgp  15366  staffval  15890  scaffval  15923  cnfldcj  16665  cnfldds  16668  xrsadd  16673  xrsmul  16674  xrsds  16696  ipffval  16834  ocvfval  16848  leordtval2  17230  iscnp2  17257  utop3cls  18234  nmfval  18589  nmoffn  18698  nmofval  18701  icccld  18754  addcnlem  18847  iimulcn  18916  icopnfhmeo  18921  iccpnfcnv  18922  iccpnfhmeo  18923  xrhmeo  18924  xrhmph  18925  oprpiece1res1  18929  oprpiece1res2  18930  ishtpy  18950  pcoass  19002  tchex  19129  cnfldcusp  19264  resscdrg  19265  vitalilem4  19456  vitalilem5  19457  mbfdm  19473  dveflem  19816  dvlipcn  19831  c1lip2  19835  dgrid  20135  iaa  20195  abelthlem3  20302  abelthlem5  20304  abelth  20310  efcn  20312  sinhalfpilem  20327  sincosq1lem  20358  sincosq4sgn  20362  tangtx  20366  sincos4thpi  20374  sincos6thpi  20376  pige3  20378  relogcn  20482  dvlog2lem  20496  dvlog2  20497  logtayl  20504  logtayl2  20506  cxpsqrlem  20546  cxpsqr  20547  cxpcn2  20583  cxpcn3  20585  ang180lem1  20604  ang180lem2  20605  1cubrlem  20634  mcubic  20640  quart1lem  20648  quart1  20649  reasinsin  20689  atancj  20703  efiatan  20705  atantan  20716  atanbndlem  20718  atan1  20721  atancn  20729  atantayl2  20731  log2cnv  20737  log2tlbnd  20738  log2ublem1  20739  log2ublem2  20740  log2ub  20742  rlimcnp3  20759  efrlim  20761  scvxcvx  20777  1sgm2ppw  20937  ppiub  20941  bclbnd  21017  bposlem8  21028  lgsdir2lem1  21060  lgsdir2lem5  21064  lgseisenlem1  21086  lgseisenlem2  21087  lgsquadlem1  21091  chebbnd1  21119  dchrvmasumlem2  21145  cusgrasizeindb1  21433  3v3e3cycl1  21584  constr3lem2  21586  constr3lem5  21588  constr3trllem5  21594  vdegp1ai  21659  ex-fl  21708  0vfval  22038  smcnlem  22146  lnocoi  22211  nmlno0lem  22247  nmblolbii  22253  blocnilem  22258  blocni  22259  cncph  22273  isph  22276  ip0i  22279  ip1ilem  22280  ip2i  22282  ipdirilem  22283  ipasslem7  22290  ipasslem8  22291  ipasslem9  22292  ipasslem10  22293  ipasslem11  22294  ip2dii  22298  pythi  22304  siilem1  22305  siilem2  22306  siii  22307  hvmulassi  22501  hvmulcomi  22502  hvdistr1i  22506  hvsubdistr1i  22507  hvassi  22508  hvadd32i  22509  hvsubassi  22510  hvsub32i  22511  normlem0  22564  normlem8  22572  normlem9  22573  bcseqi  22575  polid2i  22612  hhph  22633  hlim0  22691  shscli  22772  shlessi  22832  shlej1i  22833  omlsilem  22857  shlubi  22870  h1de2i  23008  pjadjii  23129  pjaddii  23130  pjmulii  23132  pjdifnormii  23138  pjcji  23139  hoaddsubassi  23276  eigrei  23290  eigposi  23292  eigorthi  23293  adj0  23450  lnopeq0lem1  23461  lnopunilem1  23466  lnophmlem2  23473  nmcexi  23482  nmcopexi  23483  lnfn0i  23498  nmcfnexi  23507  mdexchi  23791  xppreima2  24013  elxrge02  24131  xrge0adddir  24168  fsumrp0cl  24170  xrnarchi  24207  zzs0  24220  re0g  24226  unitssxrge0  24251  raddcn  24268  xrge0iifcnv  24272  xrge0iifiso  24274  xrge0iifhmeo  24275  xrge0iifhom  24276  xrge0iifmhm  24278  xrge0mulc1cn  24280  lmlimxrge0  24287  pnfneige0  24289  lmxrge0  24290  zzsnm  24295  reust  24297  recusp  24298  cnzh  24307  rezh  24308  qqh0  24321  qqh1  24322  qqhucn  24329  rrhre  24340  esum0  24397  esumpinfval  24416  esumpfinvallem  24417  esummulc1  24424  hashf2  24427  esumcvg  24429  br2base  24572  sxbrsigalem3  24575  dya2iocbrsiga  24578  dya2icobrsiga  24579  sxbrsigalem1  24588  sxbrsigalem2  24589  sxbrsigalem4  24590  sxbrsigalem5  24591  sxbrsiga  24593  ballotlem2  24699  ballotlem4  24709  ballotlemi1  24713  ballotth  24748  subfacp1lem1  24818  subfacp1lem6  24824  kur14lem6  24850  cvmliftlem4  24928  fununiq  25340  ax5seglem7  25778  axlowdimlem6  25790  axlowdimlem8  25792  axlowdimlem11  25795  fvtransport  25870  bpoly3  26008  ismblfin  26146  mbfposadd  26153  dvreasin  26179  areacirclem3  26182  rrnval  26426  rabren3dioph  26766  jm2.27dlem2  26971  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  expdioph  26984  frlmbas  27091  m1expaddsub  27289  cnmsgnsubg  27302  lhe4.4ex1a  27414  itgsin0pilem1  27611  stoweidlem13  27629  wallispilem2  27682  wallispilem4  27684  wallispi2lem1  27687  stirlinglem13  27702  usg2spot2nb  28168  a9e2ndeqALT  28753  dihjatcclem4  31904
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator