MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp3an Structured version   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  3000  raltp  3855  rextp  3856  ordom  4846  funopg  5477  ftp  5909  caovass  6239  caovdi  6258  ofmres  6335  omopthlem1  6890  omopthlem2  6891  omopthi  6892  xpcomen  7191  unfilem3  7365  hartogs  7505  card2on  7514  unwf  7728  tskwe  7829  alephsmo  7975  dfac4  7995  dfac2a  8002  ackbij1lem5  8096  ackbij1lem13  8104  axdc2lem  8320  axcclem  8329  ondomon  8430  cfpwsdom  8451  pwfseqlem2  8526  pwfseqlem3  8527  1lt2pi  8774  addassi  9090  mulassi  9091  adddii  9092  adddiri  9093  lttri  9191  lelttri  9192  ltletri  9193  letri  9194  ltadd2i  9196  mul02lem2  9235  addid1  9238  addcani  9251  addcan2i  9252  mul12i  9253  mul32i  9254  add12i  9275  add32i  9276  subaddi  9379  subadd2i  9380  subsub23i  9382  addsubassi  9383  addsubi  9384  subcani  9385  subcan2i  9386  pnncani  9387  subdii  9474  subdiri  9475  ltadd1i  9573  leadd1i  9574  leadd2i  9575  ltsubaddi  9576  lesubaddi  9577  ltsubadd2i  9578  lesubadd2i  9579  ltaddsubi  9580  mulcani  9653  div23i  9764  div11i  9765  1mhlfehlf  10182  halfpm6th  10184  addex  10602  mulex  10603  unirnioo  10996  ioorebas  10998  uzenom  11296  nnenom  11311  m1expcl2  11395  i4  11475  expnass  11478  faclbnd4lem1  11576  bcn1  11596  ccatfn  11733  cats1fvn  11814  cats1fv  11815  cats1cat  11817  abs3difi  12204  0.999...  12650  geoihalfsum  12651  ef01bndlem  12777  cos1bnd  12780  cos2bnd  12781  sin4lt0  12788  rpnnen2lem3  12808  rpnnen2lem11  12816  rpnnen  12818  rexpen  12819  aleph1irr  12837  divalglem2  12907  ndvdsi  12922  gcdaddmlem  13020  bezout  13034  3prm  13088  dec2dvds  13391  modxai  13396  modsubi  13400  gcdi  13401  numexp2x  13407  prdsval  13670  prdsds  13678  mreexexd  13865  plusffval  14694  0frgp  15403  staffval  15927  scaffval  15960  cnfldcj  16702  cnfldds  16705  xrsadd  16710  xrsmul  16711  xrsds  16733  ipffval  16871  ocvfval  16885  leordtval2  17268  iscnp2  17295  utop3cls  18273  nmfval  18628  nmoffn  18737  nmofval  18740  icccld  18793  addcnlem  18886  iimulcn  18955  icopnfhmeo  18960  iccpnfcnv  18961  iccpnfhmeo  18962  xrhmeo  18963  xrhmph  18964  oprpiece1res1  18968  oprpiece1res2  18969  ishtpy  18989  pcoass  19041  tchex  19168  cnfldcusp  19303  resscdrg  19304  vitalilem4  19495  vitalilem5  19496  mbfdm  19512  dveflem  19855  dvlipcn  19870  c1lip2  19874  dgrid  20174  iaa  20234  abelthlem3  20341  abelthlem5  20343  abelth  20349  efcn  20351  sinhalfpilem  20366  sincosq1lem  20397  sincosq4sgn  20401  tangtx  20405  sincos4thpi  20413  sincos6thpi  20415  pige3  20417  relogcn  20521  dvlog2lem  20535  dvlog2  20536  logtayl  20543  logtayl2  20545  cxpsqrlem  20585  cxpsqr  20586  cxpcn2  20622  cxpcn3  20624  ang180lem1  20643  ang180lem2  20644  1cubrlem  20673  mcubic  20679  quart1lem  20687  quart1  20688  reasinsin  20728  atancj  20742  efiatan  20744  atantan  20755  atanbndlem  20757  atan1  20760  atancn  20768  atantayl2  20770  log2cnv  20776  log2tlbnd  20777  log2ublem1  20778  log2ublem2  20779  log2ub  20781  rlimcnp3  20798  efrlim  20800  scvxcvx  20816  1sgm2ppw  20976  ppiub  20980  bclbnd  21056  bposlem8  21067  lgsdir2lem1  21099  lgsdir2lem5  21103  lgseisenlem1  21125  lgseisenlem2  21126  lgsquadlem1  21130  chebbnd1  21158  dchrvmasumlem2  21184  cusgrasizeindb1  21472  3v3e3cycl1  21623  constr3lem2  21625  constr3lem5  21627  constr3trllem5  21633  vdegp1ai  21698  ex-fl  21747  0vfval  22077  smcnlem  22185  lnocoi  22250  nmlno0lem  22286  nmblolbii  22292  blocnilem  22297  blocni  22298  cncph  22312  isph  22315  ip0i  22318  ip1ilem  22319  ip2i  22321  ipdirilem  22322  ipasslem7  22329  ipasslem8  22330  ipasslem9  22331  ipasslem10  22332  ipasslem11  22333  ip2dii  22337  pythi  22343  siilem1  22344  siilem2  22345  siii  22346  hvmulassi  22540  hvmulcomi  22541  hvdistr1i  22545  hvsubdistr1i  22546  hvassi  22547  hvadd32i  22548  hvsubassi  22549  hvsub32i  22550  normlem0  22603  normlem8  22611  normlem9  22612  bcseqi  22614  polid2i  22651  hhph  22672  hlim0  22730  shscli  22811  shlessi  22871  shlej1i  22872  omlsilem  22896  shlubi  22909  h1de2i  23047  pjadjii  23168  pjaddii  23169  pjmulii  23171  pjdifnormii  23177  pjcji  23178  hoaddsubassi  23315  eigrei  23329  eigposi  23331  eigorthi  23332  adj0  23489  lnopeq0lem1  23500  lnopunilem1  23505  lnophmlem2  23512  nmcexi  23521  nmcopexi  23522  lnfn0i  23537  nmcfnexi  23546  mdexchi  23830  xppreima2  24052  elxrge02  24170  xrge0adddir  24207  fsumrp0cl  24209  xrnarchi  24246  zzs0  24259  re0g  24265  unitssxrge0  24290  raddcn  24307  xrge0iifcnv  24311  xrge0iifiso  24313  xrge0iifhmeo  24314  xrge0iifhom  24315  xrge0iifmhm  24317  xrge0mulc1cn  24319  lmlimxrge0  24326  pnfneige0  24328  lmxrge0  24329  zzsnm  24334  reust  24336  recusp  24337  cnzh  24346  rezh  24347  qqh0  24360  qqh1  24361  qqhucn  24368  rrhre  24379  esum0  24436  esumpinfval  24455  esumpfinvallem  24456  esummulc1  24463  hashf2  24466  esumcvg  24468  br2base  24611  sxbrsigalem3  24614  dya2iocbrsiga  24617  dya2icobrsiga  24618  sxbrsigalem1  24627  sxbrsigalem2  24628  sxbrsigalem4  24629  sxbrsigalem5  24630  sxbrsiga  24632  ballotlem2  24738  ballotlem4  24748  ballotlemi1  24752  ballotth  24787  subfacp1lem1  24857  subfacp1lem6  24863  kur14lem6  24889  cvmliftlem4  24967  fununiq  25386  ax5seglem7  25866  axlowdimlem6  25878  axlowdimlem8  25880  axlowdimlem11  25883  fvtransport  25958  bpoly3  26096  ismblfin  26237  mbfposadd  26244  ftc1anclem5  26274  ftc1anc  26278  dvreasin  26280  areacirclem3  26283  rrnval  26527  rabren3dioph  26867  jm2.27dlem2  27072  rmydioph  27076  rmxdioph  27078  expdiophlem2  27084  expdioph  27085  frlmbas  27191  m1expaddsub  27389  cnmsgnsubg  27402  lhe4.4ex1a  27514  itgsin0pilem1  27711  stoweidlem13  27729  wallispilem2  27782  wallispilem4  27784  wallispi2lem1  27787  stirlinglem13  27802  usg2spot2nb  28391  a9e2ndeqALT  28980  sineq0ALT  28986  dihjatcclem4  32156
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