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

Theorem anassrs 658
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anassrs.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
anassrs  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem anassrs
StepHypRef Expression
1 anassrs.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 614 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 438 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  anass  659  mpanr1  694  pm2.61ddan  806  pm2.61dda  807  anass1rs  821  anabss5  830  anabss7  835  pm2.61da2ne  2724  ralimdvva  2811  2ralbida  2841  2ralbidva  2842  2rexbidva  2919  copsexg  4701  pofun  4790  imainss  5270  eqfnfv2  6000  fnex  6157  f1elima  6189  fliftfun  6230  isores2  6249  f1oiso  6267  ovmpt2dxf  6449  grpridd  6536  sorpssuni  6607  sorpssint  6608  tfindsg2  6715  oalim  7260  omlim  7261  oaass  7288  omlimcl  7305  omass  7307  oelim2  7322  oeoa  7324  oeoelem  7325  nnaass  7349  omabs  7374  eroveu  7484  sbthlem4  7711  fimaxg  7844  fisupg  7845  fofinf1o  7878  fiming  8040  fiinfg  8041  ordtypelem7  8065  hartogs  8085  card2on  8095  unwdomg  8125  wemapwe  8228  dfac5  8585  cfsmolem  8726  isf32lem2  8810  ttukeylem6  8970  ondomon  9014  alephreg  9033  ltexprlem6  9492  recexsrlem  9553  wloglei  10174  recextlem2  10271  fimaxre  10579  creur  10631  uz11  11210  xrmaxeq  11503  xrmineq  11504  xaddf  11546  xaddass  11564  xleadd1a  11568  xlt2add  11575  xmullem  11579  xmulgt0  11598  xmulasslem3  11601  xlemul1a  11603  xadddilem  11609  fzrevral  11908  seqcaopr2  12281  expnlbnd2  12435  faclbnd4lem4  12513  rtrclreclem3  13172  rtrclreclem4  13173  relexpindlem  13175  rtrclind  13177  shftlem  13180  01sqrex  13362  cau3lem  13466  limsupbnd2  13595  limsupbnd2OLD  13596  clim2  13617  clim2c  13618  clim0c  13620  rlimresb  13678  2clim  13685  climabs0  13698  climcn1  13704  climcn2  13705  o1rlimmul  13731  climsqz  13753  climsqz2  13754  rlimsqzlem  13761  lo1le  13764  climsup  13782  caucvgrlem2  13789  iseralt  13800  summolem2  13831  fsum2dlem  13880  cvgcmp  13925  cvgcmpce  13927  climfsum  13929  fsumiun  13930  geomulcvg  13981  mertenslem2  13990  mertens  13991  prodfn0  13999  prodfrec  14000  zprod  14040  fprodeq0  14078  fprodn0  14082  fprod2dlem  14083  smu01lem  14508  gcdcllem1  14522  gcdmultiplez  14568  dvdssq  14577  lcmgcdlem  14620  lcmdvds  14622  coprmdvds2  14709  pclem  14837  pcge0  14860  pcgcd1  14875  prmpwdvds  14897  1arithlem4  14919  4sqlem18OLD  14955  4sqlem18  14961  vdwlem10  14989  vdwlem11  14990  ramval  15009  ramvalOLD  15010  ramub1lem2  15034  ramcl  15036  imasaddfnlem  15483  imasaddflem  15485  imasvscafn  15492  imasleval  15496  ismon2  15688  isepi2  15695  issubc3  15803  cofucl  15842  setcmon  16031  setcepi  16032  ipodrsfi  16458  ipodrsima  16460  isacs3lem  16461  grpidpropd  16553  gsumpropd2lem  16565  mhmpropd  16637  mhmima  16659  gsumccat  16674  grplcan  16767  mulgdirlem  16831  subgmulg  16880  issubg4  16885  subgint  16890  cycsubgcl  16892  ssnmz  16908  gastacl  17012  orbsta  17016  cntzsubg  17039  galactghm  17093  odmulg  17256  odbezout  17258  sylow3lem2  17329  lsmsubm  17354  efgsfo  17438  mulgmhm  17517  mulgghm  17518  gsumval3  17590  gsumcllem  17591  gsumpt  17643  gsum2d  17653  gsum2d2  17655  prdsgsum  17659  subgdmdprd  17716  dprd2d2  17726  ablfac1eu  17755  srglmhm  17817  srgrmhm  17818  ringpropd  17861  ringlghm  17881  dvdsrpropd  17973  abvpropd  18119  islmodd  18146  lmodprop2d  18199  lsssubg  18229  lsspropd  18289  lmhmima  18319  lsmelval2  18357  lidlsubg  18487  assapropd  18600  asclpropd  18619  psrass1lem  18650  mplcoe1  18738  mplcoe5  18741  mplind  18774  evlslem2  18784  evlsval  18791  coe1tmmul2  18918  phlpropd  19271  frlmsslsp  19403  lindfmm  19434  islindf4  19445  mamuass  19476  mavmulass  19623  mdetuni0  19695  mdetmul  19697  cpmatacl  19789  cpmadugsumfi  19950  cpmadugsum  19951  cpmadumatpolylem1  19954  cpmadumatpolylem2  19955  cpmadumatpoly  19956  cayhamlem4  19961  neips  20178  neindisj  20182  ordtrest2lem  20268  lmbrf  20325  lmss  20363  isreg2  20442  lmmo  20445  hauscmplem  20470  bwth  20474  2ndcomap  20522  1stcelcls  20525  restlly  20547  islly2  20548  cldllycmp  20559  comppfsc  20596  1stckgenlem  20617  txbas  20631  txbasval  20670  tx1cn  20673  ptpjopn  20676  ptcnp  20686  txnlly  20701  txlm  20712  xkococn  20724  fgabs  20943  fmfnfmlem4  21021  flimcf  21046  hauspwpwf1  21051  fclsbas  21085  fclscf  21089  flimfnfcls  21092  ghmcnp  21178  tsmsxp  21218  isxmet2d  21391  elmopn2  21509  mopni3  21558  blsscls2  21568  metequiv2  21574  metss2lem  21575  met2ndci  21586  metrest  21588  metcnp  21605  metcnp2  21606  metcnpi3  21610  txmetcnp  21611  nmolb2d  21772  xrge0tsms  21901  metdsre  21919  metnrmlem3  21927  metdsreOLD  21934  metnrmlem3OLD  21942  fsumcn  21951  elcncf2  21971  mulc1cncf  21986  cncfco  21988  cncfmet  21989  bndth  22035  evth  22036  copco  22098  pcopt2  22103  pcoass  22104  pcorevlem  22106  lmmcvg  22280  lmmbrf  22281  iscau4  22298  iscauf  22299  cmetcaulem  22307  iscmet3lem3  22309  iscmet3lem1  22310  causs  22317  equivcfil  22318  lmclim  22321  caubl  22326  caublcls  22327  bcth3  22348  ivthle  22456  ivthle2  22457  ovoliunlem1  22504  ovolicc2lem5  22524  volsuplem  22557  uniioombllem6  22595  dyaddisjlem  22602  dyadmax  22605  volcn  22613  mbfmulc2lem  22652  ismbf3d  22659  mbfsup  22669  mbfinf  22670  mbfinfOLD  22671  mbflim  22675  i1fmullem  22701  itg2seq  22749  itg2uba  22750  itg2splitlem  22755  itg2split  22756  itg2monolem1  22757  ditgsplitlem  22864  ellimc2  22881  ellimc3  22883  limcflf  22885  limcmpt  22887  limcco  22897  lhop1lem  23014  dvfsumle  23022  dvfsumabs  23024  dvfsumrlim  23032  ftc1a  23038  ftc1lem6  23042  mdegmullem  23076  elply2  23199  plypf1  23215  ulmcaulem  23398  ulmcau  23399  ulmss  23401  ulmdvlem3  23406  mtest  23408  itgulm  23412  abelthlem8  23443  abelth  23445  tanord  23536  cxpcn3lem  23736  mcubic  23822  cubic2  23823  dvdsflsumcom  24166  fsumdvdsmul  24173  lgsdchrval  24324  2sqlem9  24350  rplogsumlem2  24372  rpvmasumlem  24374  dchrvmasumlem1  24382  vmalogdivsum2  24425  logsqvma  24429  selberg  24435  selberg4  24448  pntibndlem3  24479  pntlem3  24496  pntleml  24498  padicabv  24517  padicabvf  24518  padicabvcxp  24519  ostth3  24525  axpasch  25020  axcontlem7  25049  axcontlem10  25052  cusgrasize2inds  25254  2spotdisj  25838  grpolcan  26010  isgrp2d  26012  ghgrpOLD  26145  nvmul0or  26322  sspival  26426  nmosetre  26454  blocnilem  26494  blocni  26495  h2hcau  26681  h2hlm  26682  shsel3  27017  chscllem2  27340  homulcl  27461  adjsym  27535  cnvadj  27594  hhcno  27606  hhcnf  27607  lnopl  27616  unoplin  27622  counop  27623  lnfnl  27633  hmoplin  27644  hmopm  27723  nmcexi  27728  lnconi  27735  riesz3i  27764  leopmuli  27835  leopmul  27836  hstle  27932  mdsl0  28012  mdslmd1lem2  28028  atcvatlem  28087  chirredi  28096  cdj1i  28135  foresf1o  28188  isoun  28331  difioo  28413  xrge0tsmsd  28597  pstmxmet  28749  ordtrest2NEWlem  28777  esum2dlem  28962  esum2d  28963  dya2icoseg2  29149  eulerpartlemgc  29244  eulerpartlemgvv  29258  eulerpartlemgh  29260  eulerpartlemgs2  29262  ballotlemimin  29387  ballotlemiminOLD  29425  signstfvneq0  29510  conpcon  30007  cvmliftmolem2  30054  cvmliftlem6  30062  cvmliftlem8  30064  cvmlift2lem10  30084  cvmlift2lem12  30086  elmrsubrn  30207  dfon2lem6  30483  poseq  30540  nocvxminlem  30628  nofulllem5  30644  ifscgr  30860  brsegle  30924  neibastop2lem  31065  finixpnum  31975  fin2solem  31976  fin2so  31977  poimirlem3  31988  poimirlem4  31989  poimirlem6  31991  poimirlem7  31992  poimirlem14  31999  poimirlem16  32001  poimirlem19  32004  poimirlem22  32007  poimirlem28  32013  poimirlem29  32014  poimirlem30  32015  poimir  32018  heicant  32020  itg2gt0cn  32042  bddiblnc  32057  ftc1cnnc  32061  ftc1anclem5  32066  ftc1anclem6  32067  ftc1anclem7  32068  ftc1anc  32070  cover2  32085  filbcmb  32112  fdc  32119  fdc1  32120  seqpo  32121  incsequz  32122  incsequz2  32123  metf1o  32129  lmclim2  32132  geomcau  32133  isbnd2  32160  bndss  32163  ismtybndlem  32183  heibor1lem  32186  rrncmslem  32209  rrnequiv  32212  exidreslem  32220  ghomco  32226  isdrngo3  32243  rngoisocnv  32265  isidlc  32293  idlnegcl  32300  divrngidl  32306  intidl  32307  unichnidl  32309  keridl  32310  igenmin  32342  prnc  32345  ispridlc  32348  prter3  32499  glbconxN  32988  atltcvr  33045  3dim1  33077  lvolnle3at  33192  linepsubN  33362  osumclN  33577  pexmidALTN  33588  lhpmatb  33641  cdlemg1idlemN  34184  dihlss  34863  dihglblem5aN  34905  dihatlat  34947  lsmfgcl  35977  kercvrlsm  35986  unxpwdom3  35998  hbt  36034  cntzsdrg  36113  cvgdvgrat  36706  climinf  37722  climinfOLD  37723  clim2f  37754  clim2cf  37769  clim0cf  37773  cusgrsize2inds  39564  mgmhmpropd  40058  mgmhmima  40075  ovmpt2rdxf  40393  cotsqcscsq  40755  aacllem  40813
  Copyright terms: Public domain W3C validator