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

Theorem mp3an 1323
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 1310 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 672 1  |-  th
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 972
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 185  df-an 371  df-3an 974
This theorem is referenced by:  vtocl3  3147  raltp  4065  rextp  4066  funopg  5606  ftp  6063  caovass  6456  caovdi  6475  ordom  6690  ofmres  6777  omopthlem1  7302  omopthlem2  7303  omopthi  7304  xpcomen  7606  unfilem3  7784  hartogs  7967  card2on  7978  unwf  8226  tskwe  8329  alephsmo  8481  dfac4  8501  dfac2a  8508  ackbij1lem5  8602  ackbij1lem13  8610  axdc2lem  8826  axcclem  8835  ondomon  8936  cfpwsdom  8957  pwfseqlem2  9035  pwfseqlem3  9036  1lt2pi  9281  addassi  9602  mulassi  9603  adddii  9604  adddiri  9605  lttri  9708  lelttri  9709  ltletri  9710  letri  9711  ltadd2iOLD  9713  ltadd2i  9714  mul02lem2  9755  addid1  9758  addcani  9771  addcan2i  9772  mul12i  9773  mul32i  9774  add12i  9796  add32i  9797  subaddi  9907  subadd2i  9908  subsub23i  9910  addsubassi  9911  addsubi  9912  subcani  9913  subcan2i  9914  pnncani  9915  subdii  10006  subdiri  10007  ltadd1i  10108  leadd1i  10109  leadd2i  10110  ltsubaddi  10111  lesubaddi  10112  ltsubadd2i  10113  lesubadd2i  10114  ltaddsubi  10115  mulcani  10189  div23i  10303  div11i  10304  1mhlfehlf  10759  halfpm6th  10761  addex  11222  mulex  11223  unirnioo  11628  ioorebas  11630  uzenom  12049  nnenom  12064  m1expcl2  12162  i4  12244  expnass  12247  faclbnd4lem1  12345  bcn1  12365  ccatfn  12565  cats1fvn  12797  cats1fv  12798  cats1cat  12800  abs3difi  13215  0.999...  13664  geoihalfsum  13665  ef01bndlem  13791  cos1bnd  13794  cos2bnd  13795  sin4lt0  13802  rpnnen2lem3  13822  rpnnen2lem11  13830  rpnnen  13832  rexpen  13833  aleph1irr  13851  divalglem2  13925  ndvdsi  13940  gcdaddmlem  14038  bezout  14052  3prm  14106  dec2dvds  14421  modxai  14426  modsubi  14430  gcdi  14431  numexp2x  14437  prdsval  14724  prdsds  14733  mreexexd  14917  plusffval  15746  pmtrprfval  16381  m1expaddsub  16392  0frgp  16666  staffval  17364  scaffval  17398  cnfldcj  18295  cnfldds  18298  xrsadd  18303  xrsmul  18304  xrsds  18329  nn0srg  18354  rge0srg  18355  zring0  18366  zrng0  18372  cnmsgnsubg  18480  psgninv  18485  re0g  18515  ipffval  18550  ocvfval  18564  frlmbas  18653  frlmbasOLD  18654  mdetrlin  18971  mdetunilem9  18989  leordtval2  19579  iscnp2  19606  utop3cls  20620  nmfval  20975  nmoffn  21084  nmofval  21087  icccld  21140  addcnlem  21234  iimulcn  21304  icopnfhmeo  21309  iccpnfcnv  21310  iccpnfhmeo  21311  xrhmeo  21312  xrhmph  21313  oprpiece1res1  21317  oprpiece1res2  21318  ishtpy  21338  pcoass  21390  tchex  21526  cnfldcusp  21663  resscdrg  21664  reust  21679  recusp  21680  vitalilem4  21886  vitalilem5  21887  mbfdm  21901  dveflem  22246  dvlipcn  22261  c1lip2  22265  dgrid  22526  iaa  22586  abelthlem3  22693  abelthlem5  22695  abelth  22701  efcn  22703  sinhalfpilem  22721  sincosq1lem  22755  sincosq4sgn  22759  tangtx  22763  sincos4thpi  22771  sincos6thpi  22773  pige3  22775  relogcn  22884  dvlog2lem  22898  dvlog2  22899  logtayl  22906  logtayl2  22908  cxpsqrtlem  22948  cxpsqrt  22949  cxpcn2  22985  cxpcn3  22987  ang180lem1  23006  ang180lem2  23007  1cubrlem  23037  mcubic  23043  quart1lem  23051  quart1  23052  reasinsin  23092  atancj  23106  efiatan  23108  atantan  23119  atanbndlem  23121  atan1  23124  atancn  23132  atantayl2  23134  log2cnv  23140  log2tlbnd  23141  log2ublem1  23142  log2ublem2  23143  log2ub  23145  efrlim  23164  scvxcvx  23180  1sgm2ppw  23340  ppiub  23344  bclbnd  23420  bposlem8  23431  lgsdir2lem1  23463  lgsdir2lem5  23467  lgseisenlem1  23489  lgseisenlem2  23490  lgsquadlem1  23494  chebbnd1  23522  dchrvmasumlem2  23548  trgcgrg  23771  ax5seglem7  24103  axlowdimlem6  24115  axlowdimlem8  24117  axlowdimlem11  24120  cusgrasizeindb1  24336  3v3e3cycl1  24509  constr3lem2  24511  constr3lem5  24513  constr3trllem5  24519  erclwwlktr  24680  erclwwlkntr  24692  0egra0rgra  24801  vdegp1ai  24849  usg2spot2nb  24930  ex-fl  25033  0vfval  25364  smcnlem  25472  lnocoi  25537  nmlno0lem  25573  nmblolbii  25579  blocnilem  25584  blocni  25585  cncph  25599  isph  25602  ip0i  25605  ip1ilem  25606  ip2i  25608  ipdirilem  25609  ipasslem7  25616  ipasslem8  25617  ipasslem9  25618  ipasslem10  25619  ipasslem11  25620  ip2dii  25624  pythi  25630  siilem1  25631  siilem2  25632  siii  25633  hvmulassi  25828  hvmulcomi  25829  hvdistr1i  25833  hvsubdistr1i  25834  hvassi  25835  hvadd32i  25836  hvsubassi  25837  hvsub32i  25838  normlem0  25891  normlem8  25899  normlem9  25900  bcseqi  25902  polid2i  25939  hhph  25960  hlim0  26018  shscli  26100  shlessi  26160  shlej1i  26161  omlsilem  26185  shlubi  26198  h1de2i  26336  pjadjii  26457  pjaddii  26458  pjmulii  26460  pjdifnormii  26466  pjcji  26467  hoaddsubassi  26604  eigrei  26618  eigposi  26620  eigorthi  26621  adj0  26778  lnopeq0lem1  26789  lnopunilem1  26794  lnophmlem2  26801  nmcexi  26810  nmcopexi  26811  lnfn0i  26826  nmcfnexi  26835  mdexchi  27119  xppreima2  27353  elxrge02  27494  xrge0adddir  27548  xrnarchi  27594  xrge0slmod  27700  raddcn  27777  xrge0iifcnv  27781  xrge0iifiso  27783  xrge0iifhmeo  27784  xrge0iifhom  27785  xrge0iifmhm  27787  xrge0mulc1cn  27789  lmlimxrge0  27796  pnfneige0  27799  lmxrge0  27800  zringnm  27806  zzsnmOLD  27808  rezh  27818  qqh0  27831  qqh1  27832  qqhucn  27839  esumpinfval  27945  hashf2  27956  esumcvg  27958  br2base  28106  sxbrsigalem3  28109  dya2iocbrsiga  28112  dya2icobrsiga  28113  sxbrsigalem1  28122  sxbrsigalem2  28123  sxbrsigalem4  28124  sxbrsigalem5  28125  sxbrsiga  28127  ballotlem2  28293  ballotlem4  28303  ballotlemi1  28307  ballotth  28342  sgnclre  28344  signstf  28389  subfacp1lem1  28489  subfacp1lem6  28495  kur14lem6  28521  cvmliftlem4  28599  problem4  28888  quad3  28890  fununiq  29168  fvtransport  29650  bpoly3  29788  cos2h  30014  tan2h  30015  ismblfin  30023  mbfposadd  30030  ftc1anclem5  30062  asindmre  30070  dvasin  30071  dvacos  30072  rrnval  30291  rabren3dioph  30717  jm2.27dlem2  30920  rmydioph  30924  rmxdioph  30926  expdiophlem2  30932  expdioph  30933  arearect  31152  areaquad  31153  lhe4.4ex1a  31203  lptioo2cn  31555  icccncfext  31593  itgsin0pilem1  31634  itgsbtaddcnst  31667  stoweidlem13  31680  wallispilem2  31733  wallispilem4  31735  wallispi2lem1  31738  stirlinglem13  31753  dirkerper  31763  dirkertrigeqlem3  31767  dirkeritg  31769  dirkercncflem1  31770  dirkercncflem4  31773  fourierdlem42  31816  fourierdlem62  31836  fourierdlem102  31876  fourierdlem103  31877  fourierdlem104  31878  fourierdlem114  31888  sqwvfoura  31896  fourierswlem  31898  fouriersw  31899  0nodd  32331  oddinmgm  32336  2zrng0  32444  zlmodzxz0  32653  zlmodzxzequa  32807  zlmodzxzequap  32810  zlmodzxzldeplem3  32813  ax6e2ndeqALT  33439  sineq0ALT  33445  bj-minftyccb  34330  dihjatcclem4  36850  taupilem2  37399
  Copyright terms: Public domain W3C validator