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

Theorem mp3an 1277
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 1264 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 653 1  |-  th
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  vtocl3  2853  raltp  3701  rextp  3702  ordom  4681  funopg  5302  caovass  6036  caovdi  6055  ofmres  6132  omopthlem1  6669  omopthlem2  6670  omopthi  6671  xpcomen  6969  unfilem3  7139  hartogs  7275  card2on  7284  unwf  7498  tskwe  7599  alephsmo  7745  dfac4  7765  dfac2a  7772  ackbij1lem5  7866  ackbij1lem13  7874  axdc2lem  8090  axcclem  8099  ondomon  8201  cfpwsdom  8222  pwfseqlem2  8297  pwfseqlem3  8298  1lt2pi  8545  addassi  8861  mulassi  8862  adddii  8863  adddiri  8864  lttri  8961  lelttri  8962  ltletri  8963  letri  8964  ltadd2i  8966  mul02lem2  9005  addid1  9008  addcani  9021  addcan2i  9022  mul12i  9023  mul32i  9024  add12i  9045  add32i  9046  subaddi  9149  subadd2i  9150  subsub23i  9152  addsubassi  9153  addsubi  9154  subcani  9155  subcan2i  9156  pnncani  9157  subdii  9244  subdiri  9245  ltadd1i  9343  leadd1i  9344  leadd2i  9345  ltsubaddi  9346  lesubaddi  9347  ltsubadd2i  9348  lesubadd2i  9349  ltaddsubi  9350  mulcani  9423  div23i  9534  div11i  9535  1mhlfehlf  9950  halfpm6th  9952  addex  10368  mulex  10369  unirnioo  10759  ioorebas  10761  uzenom  11043  nnenom  11058  m1expcl2  11141  i4  11221  expnass  11224  faclbnd4lem1  11322  bcn1  11341  ccatfn  11443  cats1fvn  11524  cats1fv  11525  cats1cat  11527  abs3difi  11908  0.999...  12353  geoihalfsum  12354  ef01bndlem  12480  cos1bnd  12483  cos2bnd  12484  sin4lt0  12491  rpnnen2lem3  12511  rpnnen2lem11  12519  rpnnen  12521  rexpen  12522  aleph1irr  12540  divalglem2  12610  ndvdsi  12625  gcdaddmlem  12723  bezout  12737  3prm  12791  dec2dvds  13094  modxai  13099  modsubi  13103  gcdi  13104  numexp2x  13110  prdsval  13371  prdsds  13379  mreexexd  13566  plusffval  14395  0frgp  15104  staffval  15628  scaffval  15661  cnfldcj  16402  cnfldds  16405  xrsadd  16407  xrsmul  16408  xrsds  16430  ipffval  16568  ocvfval  16582  leordtval2  16958  iscnp2  16985  nmfval  18127  nmoffn  18236  nmofval  18239  icccld  18292  addcnlem  18384  iimulcn  18452  icopnfhmeo  18457  iccpnfcnv  18458  iccpnfhmeo  18459  xrhmeo  18460  xrhmph  18461  oprpiece1res1  18465  oprpiece1res2  18466  ishtpy  18486  pcoass  18538  tchex  18665  resscdrg  18791  vitalilem4  18982  vitalilem5  18983  mbfdm  18999  dveflem  19342  dvlipcn  19357  c1lip2  19361  dgrid  19661  iaa  19721  abelthlem3  19825  abelthlem5  19827  abelth  19833  efcn  19835  sinhalfpilem  19850  sincosq1lem  19881  sincosq4sgn  19885  tangtx  19889  sincos4thpi  19897  sincos6thpi  19899  pige3  19901  relogcn  20001  dvlog2lem  20015  dvlog2  20016  logtayl  20023  logtayl2  20025  cxpsqrlem  20065  cxpsqr  20066  cxpcn2  20102  cxpcn3  20104  ang180lem1  20123  ang180lem2  20124  1cubrlem  20153  mcubic  20159  quart1lem  20167  quart1  20168  reasinsin  20208  atancj  20222  efiatan  20224  atantan  20235  atanbndlem  20237  atan1  20240  atancn  20248  atantayl2  20250  log2cnv  20256  log2tlbnd  20257  log2ublem1  20258  log2ublem2  20259  log2ub  20261  rlimcnp3  20278  efrlim  20280  scvxcvx  20296  1sgm2ppw  20455  ppiub  20459  bclbnd  20535  bposlem8  20546  lgsdir2lem1  20578  lgsdir2lem5  20582  lgseisenlem1  20604  lgseisenlem2  20605  lgsquadlem1  20609  chebbnd1  20637  dchrvmasumlem2  20663  ex-fl  20850  0vfval  21178  smcnlem  21286  lnocoi  21351  nmlno0lem  21387  nmblolbii  21393  blocnilem  21398  blocni  21399  cncph  21413  isph  21416  ip0i  21419  ip1ilem  21420  ip2i  21422  ipdirilem  21423  ipasslem7  21430  ipasslem8  21431  ipasslem9  21432  ipasslem10  21433  ipasslem11  21434  ip2dii  21438  pythi  21444  siilem1  21445  siilem2  21446  siii  21447  hvmulassi  21641  hvmulcomi  21642  hvdistr1i  21646  hvsubdistr1i  21647  hvassi  21648  hvadd32i  21649  hvsubassi  21650  hvsub32i  21651  normlem0  21704  normlem8  21712  normlem9  21713  bcseqi  21715  polid2i  21752  hhph  21773  hlim0  21831  shscli  21912  shlessi  21972  shlej1i  21973  omlsilem  21997  shlubi  22010  h1de2i  22148  pjadjii  22269  pjaddii  22270  pjmulii  22272  pjdifnormii  22278  pjcji  22279  hoaddsubassi  22416  eigrei  22430  eigposi  22432  eigorthi  22433  adj0  22590  lnopeq0lem1  22601  lnopunilem1  22606  lnophmlem2  22613  nmcexi  22622  nmcopexi  22623  lnfn0i  22638  nmcfnexi  22647  mdexchi  22931  ballotlem4  23073  ballotlemi1  23077  ballotth  23112  elxrge02  23132  xppreima2  23227  unitssxrge0  23299  raddcn  23317  xrge0iifcnv  23330  xrge0iifiso  23332  xrge0iifhmeo  23333  xrge0iifhom  23334  xrge0iifmhm  23336  xrge0mulc1cn  23338  xrge0adddir  23347  fsumrp0cl  23349  lmlimxrge0  23387  pnfneige0  23389  lmxrge0  23390  esum0  23443  esumpinfval  23456  esumpfinvallem  23457  esummulc1  23464  hashf2  23467  esumcvg  23469  br2base  23589  dya2iocbrsiga  23593  coinflippvt  23700  subfacp1lem1  23725  subfacp1lem6  23731  kur14lem6  23757  cvmliftlem4  23834  vdegp1ai  23923  fununiq  24197  ax5seglem7  24635  axlowdimlem6  24647  axlowdimlem8  24649  axlowdimlem11  24652  fvtransport  24727  bpoly3  24865  dvreasin  25026  areacirclem3  25029  nZdef  25283  vecval3b  25555  cntrset  25705  addcanri  25769  dualded  25886  dualcat2  25887  pfsubkl  26150  pvp  26151  pgapspf  26155  pgapspf2  26156  rrnval  26654  rabren3dioph  27001  jm2.27dlem2  27206  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218  expdioph  27219  frlmbas  27326  m1expaddsub  27524  cnmsgnsubg  27537  lhe4.4ex1a  27649  3v3e3cycl1  28390  constr3lem2  28392  constr3lem5  28394  constr3trllem5  28400  a9e2ndeqALT  29024  dihjatcclem4  32233
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator