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

Theorem mp3an 1280
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 1267 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 655 1  |-  th
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  vtocl3  3010  raltp  3865  rextp  3866  ordom  4857  funopg  5488  ftp  5920  caovass  6250  caovdi  6269  ofmres  6346  omopthlem1  6901  omopthlem2  6902  omopthi  6903  xpcomen  7202  unfilem3  7376  hartogs  7516  card2on  7525  unwf  7739  tskwe  7842  alephsmo  7988  dfac4  8008  dfac2a  8015  ackbij1lem5  8109  ackbij1lem13  8117  axdc2lem  8333  axcclem  8342  ondomon  8443  cfpwsdom  8464  pwfseqlem2  8539  pwfseqlem3  8540  1lt2pi  8787  addassi  9103  mulassi  9104  adddii  9105  adddiri  9106  lttri  9204  lelttri  9205  ltletri  9206  letri  9207  ltadd2i  9209  mul02lem2  9248  addid1  9251  addcani  9264  addcan2i  9265  mul12i  9266  mul32i  9267  add12i  9288  add32i  9289  subaddi  9392  subadd2i  9393  subsub23i  9395  addsubassi  9396  addsubi  9397  subcani  9398  subcan2i  9399  pnncani  9400  subdii  9487  subdiri  9488  ltadd1i  9586  leadd1i  9587  leadd2i  9588  ltsubaddi  9589  lesubaddi  9590  ltsubadd2i  9591  lesubadd2i  9592  ltaddsubi  9593  mulcani  9666  div23i  9777  div11i  9778  1mhlfehlf  10195  halfpm6th  10197  addex  10615  mulex  10616  unirnioo  11009  ioorebas  11011  uzenom  11309  nnenom  11324  m1expcl2  11408  i4  11488  expnass  11491  faclbnd4lem1  11589  bcn1  11609  ccatfn  11746  cats1fvn  11827  cats1fv  11828  cats1cat  11830  abs3difi  12217  0.999...  12663  geoihalfsum  12664  ef01bndlem  12790  cos1bnd  12793  cos2bnd  12794  sin4lt0  12801  rpnnen2lem3  12821  rpnnen2lem11  12829  rpnnen  12831  rexpen  12832  aleph1irr  12850  divalglem2  12920  ndvdsi  12935  gcdaddmlem  13033  bezout  13047  3prm  13101  dec2dvds  13404  modxai  13409  modsubi  13413  gcdi  13414  numexp2x  13420  prdsval  13683  prdsds  13691  mreexexd  13878  plusffval  14707  0frgp  15416  staffval  15940  scaffval  15973  cnfldcj  16715  cnfldds  16718  xrsadd  16723  xrsmul  16724  xrsds  16746  ipffval  16884  ocvfval  16898  leordtval2  17281  iscnp2  17308  utop3cls  18286  nmfval  18641  nmoffn  18750  nmofval  18753  icccld  18806  addcnlem  18899  iimulcn  18968  icopnfhmeo  18973  iccpnfcnv  18974  iccpnfhmeo  18975  xrhmeo  18976  xrhmph  18977  oprpiece1res1  18981  oprpiece1res2  18982  ishtpy  19002  pcoass  19054  tchex  19181  cnfldcusp  19316  resscdrg  19317  vitalilem4  19508  vitalilem5  19509  mbfdm  19523  dveflem  19868  dvlipcn  19883  c1lip2  19887  dgrid  20187  iaa  20247  abelthlem3  20354  abelthlem5  20356  abelth  20362  efcn  20364  sinhalfpilem  20379  sincosq1lem  20410  sincosq4sgn  20414  tangtx  20418  sincos4thpi  20426  sincos6thpi  20428  pige3  20430  relogcn  20534  dvlog2lem  20548  dvlog2  20549  logtayl  20556  logtayl2  20558  cxpsqrlem  20598  cxpsqr  20599  cxpcn2  20635  cxpcn3  20637  ang180lem1  20656  ang180lem2  20657  1cubrlem  20686  mcubic  20692  quart1lem  20700  quart1  20701  reasinsin  20741  atancj  20755  efiatan  20757  atantan  20768  atanbndlem  20770  atan1  20773  atancn  20781  atantayl2  20783  log2cnv  20789  log2tlbnd  20790  log2ublem1  20791  log2ublem2  20792  log2ub  20794  rlimcnp3  20811  efrlim  20813  scvxcvx  20829  1sgm2ppw  20989  ppiub  20993  bclbnd  21069  bposlem8  21080  lgsdir2lem1  21112  lgsdir2lem5  21116  lgseisenlem1  21138  lgseisenlem2  21139  lgsquadlem1  21143  chebbnd1  21171  dchrvmasumlem2  21197  cusgrasizeindb1  21485  3v3e3cycl1  21636  constr3lem2  21638  constr3lem5  21640  constr3trllem5  21646  vdegp1ai  21711  ex-fl  21760  0vfval  22090  smcnlem  22198  lnocoi  22263  nmlno0lem  22299  nmblolbii  22305  blocnilem  22310  blocni  22311  cncph  22325  isph  22328  ip0i  22331  ip1ilem  22332  ip2i  22334  ipdirilem  22335  ipasslem7  22342  ipasslem8  22343  ipasslem9  22344  ipasslem10  22345  ipasslem11  22346  ip2dii  22350  pythi  22356  siilem1  22357  siilem2  22358  siii  22359  hvmulassi  22553  hvmulcomi  22554  hvdistr1i  22558  hvsubdistr1i  22559  hvassi  22560  hvadd32i  22561  hvsubassi  22562  hvsub32i  22563  normlem0  22616  normlem8  22624  normlem9  22625  bcseqi  22627  polid2i  22664  hhph  22685  hlim0  22743  shscli  22824  shlessi  22884  shlej1i  22885  omlsilem  22909  shlubi  22922  h1de2i  23060  pjadjii  23181  pjaddii  23182  pjmulii  23184  pjdifnormii  23190  pjcji  23191  hoaddsubassi  23328  eigrei  23342  eigposi  23344  eigorthi  23345  adj0  23502  lnopeq0lem1  23513  lnopunilem1  23518  lnophmlem2  23525  nmcexi  23534  nmcopexi  23535  lnfn0i  23550  nmcfnexi  23559  mdexchi  23843  xppreima2  24065  elxrge02  24183  xrge0adddir  24220  fsumrp0cl  24222  xrnarchi  24259  zzs0  24272  re0g  24278  unitssxrge0  24303  raddcn  24320  xrge0iifcnv  24324  xrge0iifiso  24326  xrge0iifhmeo  24327  xrge0iifhom  24328  xrge0iifmhm  24330  xrge0mulc1cn  24332  lmlimxrge0  24339  pnfneige0  24341  lmxrge0  24342  zzsnm  24347  reust  24349  recusp  24350  cnzh  24359  rezh  24360  qqh0  24373  qqh1  24374  qqhucn  24381  rrhre  24392  esum0  24449  esumpinfval  24468  esumpfinvallem  24469  esummulc1  24476  hashf2  24479  esumcvg  24481  br2base  24624  sxbrsigalem3  24627  dya2iocbrsiga  24630  dya2icobrsiga  24631  sxbrsigalem1  24640  sxbrsigalem2  24641  sxbrsigalem4  24642  sxbrsigalem5  24643  sxbrsiga  24645  ballotlem2  24751  ballotlem4  24761  ballotlemi1  24765  ballotth  24800  subfacp1lem1  24870  subfacp1lem6  24876  kur14lem6  24902  cvmliftlem4  24980  fununiq  25399  ax5seglem7  25879  axlowdimlem6  25891  axlowdimlem8  25893  axlowdimlem11  25896  fvtransport  25971  bpoly3  26109  cos2h  26251  tan2h  26252  ismblfin  26259  mbfposadd  26266  ftc1anclem5  26298  ftc1anc  26302  dvreasin  26304  rrnval  26550  rabren3dioph  26890  jm2.27dlem2  27095  rmydioph  27099  rmxdioph  27101  expdiophlem2  27107  expdioph  27108  frlmbas  27214  m1expaddsub  27412  cnmsgnsubg  27425  lhe4.4ex1a  27537  itgsin0pilem1  27734  stoweidlem13  27752  wallispilem2  27805  wallispilem4  27807  wallispi2lem1  27810  stirlinglem13  27825  0egra0rgra  28447  usg2spot2nb  28528  a9e2ndeqALT  29117  sineq0ALT  29123  dihjatcclem4  32293
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator