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  2840  raltp  3688  rextp  3689  ordom  4665  funopg  5286  caovass  6020  caovdi  6039  ofmres  6116  omopthlem1  6653  omopthlem2  6654  omopthi  6655  xpcomen  6953  unfilem3  7123  hartogs  7259  card2on  7268  unwf  7482  tskwe  7583  alephsmo  7729  dfac4  7749  dfac2a  7756  ackbij1lem5  7850  ackbij1lem13  7858  axdc2lem  8074  axcclem  8083  ondomon  8185  cfpwsdom  8206  pwfseqlem2  8281  pwfseqlem3  8282  1lt2pi  8529  addassi  8845  mulassi  8846  adddii  8847  adddiri  8848  lttri  8945  lelttri  8946  ltletri  8947  letri  8948  ltadd2i  8950  mul02lem2  8989  addid1  8992  addcani  9005  addcan2i  9006  mul12i  9007  mul32i  9008  add12i  9029  add32i  9030  subaddi  9133  subadd2i  9134  subsub23i  9136  addsubassi  9137  addsubi  9138  subcani  9139  subcan2i  9140  pnncani  9141  subdii  9228  subdiri  9229  ltadd1i  9327  leadd1i  9328  leadd2i  9329  ltsubaddi  9330  lesubaddi  9331  ltsubadd2i  9332  lesubadd2i  9333  ltaddsubi  9334  mulcani  9407  div23i  9518  div11i  9519  1mhlfehlf  9934  halfpm6th  9936  addex  10352  mulex  10353  unirnioo  10743  ioorebas  10745  uzenom  11027  nnenom  11042  m1expcl2  11125  i4  11205  expnass  11208  faclbnd4lem1  11306  bcn1  11325  ccatfn  11427  cats1fvn  11508  cats1fv  11509  cats1cat  11511  abs3difi  11892  0.999...  12337  geoihalfsum  12338  ef01bndlem  12464  cos1bnd  12467  cos2bnd  12468  sin4lt0  12475  rpnnen2lem3  12495  rpnnen2lem11  12503  rpnnen  12505  rexpen  12506  aleph1irr  12524  divalglem2  12594  ndvdsi  12609  gcdaddmlem  12707  bezout  12721  3prm  12775  dec2dvds  13078  modxai  13083  modsubi  13087  gcdi  13088  numexp2x  13094  prdsval  13355  prdsds  13363  mreexexd  13550  plusffval  14379  0frgp  15088  staffval  15612  scaffval  15645  cnfldcj  16386  cnfldds  16389  xrsadd  16391  xrsmul  16392  xrsds  16414  ipffval  16552  ocvfval  16566  leordtval2  16942  iscnp2  16969  nmfval  18111  nmoffn  18220  nmofval  18223  icccld  18276  addcnlem  18368  iimulcn  18436  icopnfhmeo  18441  iccpnfcnv  18442  iccpnfhmeo  18443  xrhmeo  18444  xrhmph  18445  oprpiece1res1  18449  oprpiece1res2  18450  ishtpy  18470  pcoass  18522  tchex  18649  resscdrg  18775  vitalilem4  18966  vitalilem5  18967  mbfdm  18983  dveflem  19326  dvlipcn  19341  c1lip2  19345  dgrid  19645  iaa  19705  abelthlem3  19809  abelthlem5  19811  abelth  19817  efcn  19819  sinhalfpilem  19834  sincosq1lem  19865  sincosq4sgn  19869  tangtx  19873  sincos4thpi  19881  sincos6thpi  19883  pige3  19885  relogcn  19985  dvlog2lem  19999  dvlog2  20000  logtayl  20007  logtayl2  20009  cxpsqrlem  20049  cxpsqr  20050  cxpcn2  20086  cxpcn3  20088  ang180lem1  20107  ang180lem2  20108  1cubrlem  20137  mcubic  20143  quart1lem  20151  quart1  20152  reasinsin  20192  atancj  20206  efiatan  20208  atantan  20219  atanbndlem  20221  atan1  20224  atancn  20232  atantayl2  20234  log2cnv  20240  log2tlbnd  20241  log2ublem1  20242  log2ublem2  20243  log2ub  20245  rlimcnp3  20262  efrlim  20264  scvxcvx  20280  1sgm2ppw  20439  ppiub  20443  bclbnd  20519  bposlem8  20530  lgsdir2lem1  20562  lgsdir2lem5  20566  lgseisenlem1  20588  lgseisenlem2  20589  lgsquadlem1  20593  chebbnd1  20621  dchrvmasumlem2  20647  ex-fl  20834  0vfval  21162  smcnlem  21270  lnocoi  21335  nmlno0lem  21371  nmblolbii  21377  blocnilem  21382  blocni  21383  cncph  21397  isph  21400  ip0i  21403  ip1ilem  21404  ip2i  21406  ipdirilem  21407  ipasslem7  21414  ipasslem8  21415  ipasslem9  21416  ipasslem10  21417  ipasslem11  21418  ip2dii  21422  pythi  21428  siilem1  21429  siilem2  21430  siii  21431  hvmulassi  21625  hvmulcomi  21626  hvdistr1i  21630  hvsubdistr1i  21631  hvassi  21632  hvadd32i  21633  hvsubassi  21634  hvsub32i  21635  normlem0  21688  normlem8  21696  normlem9  21697  bcseqi  21699  polid2i  21736  hhph  21757  hlim0  21815  shscli  21896  shlessi  21956  shlej1i  21957  omlsilem  21981  shlubi  21994  h1de2i  22132  pjadjii  22253  pjaddii  22254  pjmulii  22256  pjdifnormii  22262  pjcji  22263  hoaddsubassi  22400  eigrei  22414  eigposi  22416  eigorthi  22417  adj0  22574  lnopeq0lem1  22585  lnopunilem1  22590  lnophmlem2  22597  nmcexi  22606  nmcopexi  22607  lnfn0i  22622  nmcfnexi  22631  mdexchi  22915  ballotlem4  23057  ballotlemi1  23061  ballotth  23096  elxrge02  23116  xppreima2  23212  unitssxrge0  23284  raddcn  23302  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhmeo  23318  xrge0iifhom  23319  xrge0iifmhm  23321  xrge0mulc1cn  23323  xrge0adddir  23332  fsumrp0cl  23334  lmlimxrge0  23372  pnfneige0  23374  lmxrge0  23375  esum0  23428  esumpinfval  23441  esumpfinvallem  23442  esummulc1  23449  hashf2  23452  esumcvg  23454  br2base  23574  dya2iocbrsiga  23578  coinflippvt  23685  subfacp1lem1  23710  subfacp1lem6  23716  kur14lem6  23742  cvmliftlem4  23819  vdegp1ai  23908  fununiq  24126  ax5seglem7  24563  axlowdimlem6  24575  axlowdimlem8  24577  axlowdimlem11  24580  fvtransport  24655  bpoly3  24793  dvreasin  24923  areacirclem3  24926  nZdef  25180  vecval3b  25452  cntrset  25602  addcanri  25666  dualded  25783  dualcat2  25784  pfsubkl  26047  pvp  26048  pgapspf  26052  pgapspf2  26053  rrnval  26551  rabren3dioph  26898  jm2.27dlem2  27103  rmydioph  27107  rmxdioph  27109  expdiophlem2  27115  expdioph  27116  frlmbas  27223  m1expaddsub  27421  cnmsgnsubg  27434  lhe4.4ex1a  27546  a9e2ndeqALT  28708  dihjatcclem4  31611
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