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

Theorem mp3an 1314
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 1301 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 672 1  |-  th
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  vtocl3  3021  raltp  3926  rextp  3927  funopg  5445  ftp  5888  caovass  6258  caovdi  6277  ordom  6480  ofmres  6568  omopthlem1  7086  omopthlem2  7087  omopthi  7088  xpcomen  7394  unfilem3  7570  hartogs  7750  card2on  7761  unwf  8009  tskwe  8112  alephsmo  8264  dfac4  8284  dfac2a  8291  ackbij1lem5  8385  ackbij1lem13  8393  axdc2lem  8609  axcclem  8618  ondomon  8719  cfpwsdom  8740  pwfseqlem2  8818  pwfseqlem3  8819  1lt2pi  9066  addassi  9386  mulassi  9387  adddii  9388  adddiri  9389  lttri  9492  lelttri  9493  ltletri  9494  letri  9495  ltadd2i  9497  mul02lem2  9538  addid1  9541  addcani  9554  addcan2i  9555  mul12i  9556  mul32i  9557  add12i  9579  add32i  9580  subaddi  9687  subadd2i  9688  subsub23i  9690  addsubassi  9691  addsubi  9692  subcani  9693  subcan2i  9694  pnncani  9695  subdii  9785  subdiri  9786  ltadd1i  9886  leadd1i  9887  leadd2i  9888  ltsubaddi  9889  lesubaddi  9890  ltsubadd2i  9891  lesubadd2i  9892  ltaddsubi  9893  mulcani  9967  div23i  10081  div11i  10082  1mhlfehlf  10536  halfpm6th  10538  addex  10981  mulex  10982  unirnioo  11381  ioorebas  11383  uzenom  11779  nnenom  11794  m1expcl2  11879  i4  11960  expnass  11963  faclbnd4lem1  12061  bcn1  12081  ccatfn  12264  cats1fvn  12477  cats1fv  12478  cats1cat  12480  abs3difi  12888  0.999...  13333  geoihalfsum  13334  ef01bndlem  13460  cos1bnd  13463  cos2bnd  13464  sin4lt0  13471  rpnnen2lem3  13491  rpnnen2lem11  13499  rpnnen  13501  rexpen  13502  aleph1irr  13520  divalglem2  13591  ndvdsi  13606  gcdaddmlem  13704  bezout  13718  3prm  13772  dec2dvds  14084  modxai  14089  modsubi  14093  gcdi  14094  numexp2x  14100  prdsval  14385  prdsds  14394  mreexexd  14578  plusffval  15419  pmtrprfval  15984  m1expaddsub  15995  0frgp  16267  staffval  16912  scaffval  16946  cnfldcj  17805  cnfldds  17808  xrsadd  17813  xrsmul  17814  xrsds  17836  nn0srg  17861  rge0srg  17862  zring0  17873  zrng0  17879  cnmsgnsubg  17987  psgninv  17992  re0g  18022  ipffval  18057  ocvfval  18071  frlmbas  18160  frlmbasOLD  18161  mdetrlin  18389  mdetunilem9  18406  leordtval2  18796  iscnp2  18823  utop3cls  19806  nmfval  20161  nmoffn  20270  nmofval  20273  icccld  20326  addcnlem  20420  iimulcn  20490  icopnfhmeo  20495  iccpnfcnv  20496  iccpnfhmeo  20497  xrhmeo  20498  xrhmph  20499  oprpiece1res1  20503  oprpiece1res2  20504  ishtpy  20524  pcoass  20576  tchex  20712  cnfldcusp  20849  resscdrg  20850  reust  20865  recusp  20866  vitalilem4  21071  vitalilem5  21072  mbfdm  21086  dveflem  21431  dvlipcn  21446  c1lip2  21450  dgrid  21711  iaa  21771  abelthlem3  21878  abelthlem5  21880  abelth  21886  efcn  21888  sinhalfpilem  21905  sincosq1lem  21939  sincosq4sgn  21943  tangtx  21947  sincos4thpi  21955  sincos6thpi  21957  pige3  21959  relogcn  22063  dvlog2lem  22077  dvlog2  22078  logtayl  22085  logtayl2  22087  cxpsqrlem  22127  cxpsqr  22128  cxpcn2  22164  cxpcn3  22166  ang180lem1  22185  ang180lem2  22186  1cubrlem  22216  mcubic  22222  quart1lem  22230  quart1  22231  reasinsin  22271  atancj  22285  efiatan  22287  atantan  22298  atanbndlem  22300  atan1  22303  atancn  22311  atantayl2  22313  log2cnv  22319  log2tlbnd  22320  log2ublem1  22321  log2ublem2  22322  log2ub  22324  efrlim  22343  scvxcvx  22359  1sgm2ppw  22519  ppiub  22523  bclbnd  22599  bposlem8  22610  lgsdir2lem1  22642  lgsdir2lem5  22646  lgseisenlem1  22668  lgseisenlem2  22669  lgsquadlem1  22673  chebbnd1  22701  dchrvmasumlem2  22727  trgcgrg  22947  ax5seglem7  23149  axlowdimlem6  23161  axlowdimlem8  23163  axlowdimlem11  23166  cusgrasizeindb1  23347  3v3e3cycl1  23498  constr3lem2  23500  constr3lem5  23502  constr3trllem5  23508  vdegp1ai  23573  ex-fl  23622  0vfval  23952  smcnlem  24060  lnocoi  24125  nmlno0lem  24161  nmblolbii  24167  blocnilem  24172  blocni  24173  cncph  24187  isph  24190  ip0i  24193  ip1ilem  24194  ip2i  24196  ipdirilem  24197  ipasslem7  24204  ipasslem8  24205  ipasslem9  24206  ipasslem10  24207  ipasslem11  24208  ip2dii  24212  pythi  24218  siilem1  24219  siilem2  24220  siii  24221  hvmulassi  24416  hvmulcomi  24417  hvdistr1i  24421  hvsubdistr1i  24422  hvassi  24423  hvadd32i  24424  hvsubassi  24425  hvsub32i  24426  normlem0  24479  normlem8  24487  normlem9  24488  bcseqi  24490  polid2i  24527  hhph  24548  hlim0  24606  shscli  24688  shlessi  24748  shlej1i  24749  omlsilem  24773  shlubi  24786  h1de2i  24924  pjadjii  25045  pjaddii  25046  pjmulii  25048  pjdifnormii  25054  pjcji  25055  hoaddsubassi  25192  eigrei  25206  eigposi  25208  eigorthi  25209  adj0  25366  lnopeq0lem1  25377  lnopunilem1  25382  lnophmlem2  25389  nmcexi  25398  nmcopexi  25399  lnfn0i  25414  nmcfnexi  25423  mdexchi  25707  xppreima2  25933  xrge0infss  26021  elxrge02  26075  xrge0adddir  26123  xrnarchi  26169  xrge0slmod  26281  raddcn  26328  xrge0iifcnv  26332  xrge0iifiso  26334  xrge0iifhmeo  26335  xrge0iifhom  26336  xrge0iifmhm  26338  xrge0mulc1cn  26340  lmlimxrge0  26347  pnfneige0  26350  lmxrge0  26351  zringnm  26357  zzsnmOLD  26359  cnzh  26368  rezh  26369  qqh0  26382  qqh1  26383  qqhucn  26390  esumpinfval  26491  hashf2  26502  esumcvg  26504  br2base  26653  sxbrsigalem3  26656  dya2iocbrsiga  26659  dya2icobrsiga  26660  sxbrsigalem1  26669  sxbrsigalem2  26670  sxbrsigalem4  26671  sxbrsigalem5  26672  sxbrsiga  26674  oms0  26679  ballotlem2  26840  ballotlem4  26850  ballotlemi1  26854  ballotth  26889  sgnclre  26891  signstf  26936  subfacp1lem1  27036  subfacp1lem6  27042  kur14lem6  27068  cvmliftlem4  27146  problem4  27270  fununiq  27550  fvtransport  28032  bpoly3  28170  cos2h  28394  tan2h  28395  ismblfin  28403  mbfposadd  28410  ftc1anclem5  28442  asindmre  28450  dvasin  28451  dvacos  28452  rrnval  28697  rabren3dioph  29125  jm2.27dlem2  29330  rmydioph  29334  rmxdioph  29336  expdiophlem2  29342  expdioph  29343  arearect  29562  areaquad  29563  lhe4.4ex1a  29574  itgsin0pilem1  29761  stoweidlem13  29779  wallispilem2  29832  wallispilem4  29834  wallispi2lem1  29837  stirlinglem13  29852  erclwwlktr  30456  erclwwlkntr  30472  0egra0rgra  30520  usg2spot2nb  30629  zlmodzxz0  30722  zlmodzxzequa  30969  zlmodzxzequap  30972  zlmodzxzldeplem3  30975  ax6e2ndeqALT  31596  sineq0ALT  31602  bj-pirp  32428  bj-minftyccb  32448  dihjatcclem4  34959  pirp  35506  taupilem2  35509
  Copyright terms: Public domain W3C validator