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

Theorem anassrs 646
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 603 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 430 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  anass  647  mpanr1  681  pm2.61ddan  790  pm2.61dda  791  anass1rs  805  anabss5  814  anabss7  819  pm2.61da2ne  2701  ralimdvva  2793  2ralbida  2823  2ralbidva  2824  2rexbidva  2899  copsexg  4647  pofun  4730  imainss  5331  eqfnfv2  5884  fnex  6040  f1elima  6072  fliftfun  6111  isores2  6130  f1oiso  6148  ovmpt2dxf  6327  grpridd  6414  sorpssuni  6488  sorpssint  6489  tfindsg2  6595  oalim  7100  omlim  7101  oaass  7128  omlimcl  7145  omass  7147  oelim2  7162  oeoa  7164  oeoelem  7165  nnaass  7189  omabs  7214  eroveu  7324  sbthlem4  7549  fimaxg  7682  fisupg  7683  fofinf1o  7716  ordtypelem7  7864  hartogs  7884  card2on  7895  unwdomg  7925  wemapwe  8052  wemapweOLD  8053  dfac5  8422  cfsmolem  8563  isf32lem2  8647  ttukeylem6  8807  ondomon  8851  alephreg  8870  ltexprlem6  9330  recexsrlem  9391  wloglei  10002  recextlem2  10097  fimaxre  10406  creur  10446  uz11  11023  xrmaxeq  11301  xrmineq  11302  xaddf  11344  xaddass  11362  xleadd1a  11366  xlt2add  11373  xmullem  11377  xmulgt0  11396  xmulasslem3  11399  xlemul1a  11401  xadddilem  11407  fzrevral  11685  seqcaopr2  12046  expnlbnd2  12199  faclbnd4lem4  12276  rtrclreclem3  12895  rtrclreclem4  12896  relexpindlem  12898  rtrclind  12900  shftlem  12903  01sqrex  13085  cau3lem  13189  limsupbnd2  13308  clim2  13329  clim2c  13330  clim0c  13332  rlimresb  13390  2clim  13397  climabs0  13410  climcn1  13416  climcn2  13417  o1rlimmul  13443  climsqz  13465  climsqz2  13466  rlimsqzlem  13473  lo1le  13476  climsup  13494  caucvgrlem2  13499  iseralt  13509  summolem2  13540  fsum2dlem  13587  cvgcmp  13632  cvgcmpce  13634  climfsum  13636  fsumiun  13637  geomulcvg  13687  mertenslem2  13696  mertens  13697  prodfn0  13705  prodfrec  13706  zprod  13746  fprodeq0  13781  fprodn0  13785  fprod2dlem  13786  smu01lem  14137  gcdcllem1  14151  gcdmultiplez  14191  dvdssq  14200  coprmdvds2  14246  pclem  14364  pcge0  14387  pcgcd1  14402  prmpwdvds  14424  1arithlem4  14446  4sqlem18  14482  vdwlem10  14510  vdwlem11  14511  ramval  14528  ramub1lem2  14547  ramcl  14549  imasaddfnlem  14935  imasaddflem  14937  imasvscafn  14944  imasleval  14948  ismon2  15140  isepi2  15147  issubc3  15255  cofucl  15294  setcmon  15483  setcepi  15484  ipodrsfi  15910  ipodrsima  15912  isacs3lem  15913  grpidpropd  16005  gsumpropd2lem  16017  mhmpropd  16089  mhmima  16111  gsumccat  16126  grplcan  16219  mulgdirlem  16283  subgmulg  16332  issubg4  16337  subgint  16342  cycsubgcl  16344  ssnmz  16360  gastacl  16464  orbsta  16468  cntzsubg  16491  galactghm  16545  odmulg  16695  odbezout  16697  sylow3lem2  16765  lsmsubm  16790  efgsfo  16874  mulgmhm  16953  mulgghm  16954  gsumval3OLD  17025  gsumval3  17028  gsumcllem  17029  gsumcllemOLD  17030  gsumpt  17102  gsumptOLD  17103  gsum2d  17113  gsum2dOLD  17114  gsum2d2  17116  prdsgsum  17120  prdsgsumOLD  17121  subgdmdprd  17194  dprd2d2  17206  ablfac1eu  17237  srglmhm  17299  srgrmhm  17300  ringpropd  17343  ringlghm  17363  dvdsrpropd  17458  abvpropd  17604  islmodd  17631  lmodprop2d  17685  lsssubg  17716  lsspropd  17776  lmhmima  17806  lsmelval2  17844  lidlsubg  17975  assapropd  18089  asclpropd  18108  psrass1lem  18142  mplcoe1  18240  mplcoe5  18244  mplcoe2OLD  18246  mplind  18280  evlslem2  18293  evlsval  18301  coe1tmmul2  18430  phlpropd  18781  frlmsslsp  18916  lindfmm  18947  islindf4  18958  mamuass  18989  mavmulass  19136  mdetuni0  19208  mdetmul  19210  cpmatacl  19302  cpmadugsumfi  19463  cpmadugsum  19464  cpmadumatpolylem1  19467  cpmadumatpolylem2  19468  cpmadumatpoly  19469  cayhamlem4  19474  neips  19700  neindisj  19704  ordtrest2lem  19790  lmbrf  19847  lmss  19885  isreg2  19964  lmmo  19967  hauscmplem  19992  bwth  19996  2ndcomap  20044  1stcelcls  20047  restlly  20069  islly2  20070  cldllycmp  20081  comppfsc  20118  1stckgenlem  20139  txbas  20153  txbasval  20192  tx1cn  20195  ptpjopn  20198  ptcnp  20208  txnlly  20223  txlm  20234  xkococn  20246  fgabs  20465  fmfnfmlem4  20543  flimcf  20568  hauspwpwf1  20573  fclsbas  20607  fclscf  20611  flimfnfcls  20614  ghmcnp  20698  tsmsxp  20742  isxmet2d  20915  elmopn2  21033  mopni3  21082  blsscls2  21092  metequiv2  21098  metss2lem  21099  met2ndci  21110  metrest  21112  metcnp  21129  metcnp2  21130  metcnpi3  21134  txmetcnp  21135  nmolb2d  21310  xrge0tsms  21424  metdsre  21442  metnrmlem3  21450  fsumcn  21459  elcncf2  21479  mulc1cncf  21494  cncfco  21496  cncfmet  21497  bndth  21543  evth  21544  copco  21603  pcopt2  21608  pcoass  21609  pcorevlem  21611  lmmcvg  21785  lmmbrf  21786  iscau4  21803  iscauf  21804  cmetcaulem  21812  iscmet3lem3  21814  iscmet3lem1  21815  causs  21822  equivcfil  21823  lmclim  21826  caubl  21831  caublcls  21832  bcth3  21855  ivthle  21953  ivthle2  21954  ovoliunlem1  21998  ovolicc2lem5  22017  volsuplem  22050  uniioombllem6  22082  dyaddisjlem  22089  dyadmax  22092  volcn  22100  mbfmulc2lem  22139  ismbf3d  22146  mbfsup  22156  mbfinf  22157  mbflim  22160  i1fmullem  22186  itg2seq  22234  itg2uba  22235  itg2splitlem  22240  itg2split  22241  itg2monolem1  22242  ditgsplitlem  22349  ellimc2  22366  ellimc3  22368  limcflf  22370  limcmpt  22372  limcco  22382  lhop1lem  22499  dvfsumle  22507  dvfsumabs  22509  dvfsumrlim  22517  ftc1a  22523  ftc1lem6  22527  mdegmullem  22563  elply2  22678  plypf1  22694  ulmcaulem  22874  ulmcau  22875  ulmss  22877  ulmdvlem3  22882  mtest  22884  itgulm  22888  abelthlem8  22919  abelth  22921  tanord  23010  cxpcn3lem  23208  mcubic  23294  cubic2  23295  dvdsflsumcom  23581  fsumdvdsmul  23588  lgsdchrval  23739  2sqlem9  23765  rplogsumlem2  23787  rpvmasumlem  23789  dchrvmasumlem1  23797  vmalogdivsum2  23840  logsqvma  23844  selberg  23850  selberg4  23863  pntibndlem3  23894  pntlem3  23911  pntleml  23913  padicabv  23932  padicabvf  23933  padicabvcxp  23934  ostth3  23940  axpasch  24365  axcontlem7  24394  axcontlem10  24397  cusgrasize2inds  24598  2spotdisj  25182  grpolcan  25352  isgrp2d  25354  ghgrpOLD  25487  nvmul0or  25664  sspival  25768  nmosetre  25796  blocnilem  25836  blocni  25837  h2hcau  26013  h2hlm  26014  shsel3  26350  chscllem2  26673  homulcl  26794  adjsym  26868  cnvadj  26927  hhcno  26939  hhcnf  26940  lnopl  26949  unoplin  26955  counop  26956  lnfnl  26966  hmoplin  26977  hmopm  27056  nmcexi  27061  lnconi  27068  riesz3i  27097  leopmuli  27168  leopmul  27169  hstle  27265  mdsl0  27345  mdslmd1lem2  27361  atcvatlem  27420  chirredi  27429  cdj1i  27468  foresf1o  27521  isoun  27667  difioo  27746  xrge0tsmsd  27929  pstmxmet  28030  ordtrest2NEWlem  28058  esum2dlem  28240  esum2d  28241  dya2icoseg2  28405  eulerpartlemgc  28484  eulerpartlemgvv  28498  eulerpartlemgh  28500  eulerpartlemgs2  28502  ballotlemimin  28627  signstfvneq0  28712  conpcon  28869  cvmliftmolem2  28916  cvmliftlem6  28924  cvmliftlem8  28926  cvmlift2lem10  28946  cvmlift2lem12  28948  elmrsubrn  29069  dfon2lem6  29385  poseq  29498  nocvxminlem  29615  nofulllem5  29631  ifscgr  29847  brsegle  29911  finixpnum  30203  fin2solem  30204  fin2so  30205  heicant  30214  itg2gt0cn  30236  bddiblnc  30251  ftc1cnnc  30255  ftc1anclem5  30260  ftc1anclem6  30261  ftc1anclem7  30262  ftc1anc  30264  neibastop2lem  30344  cover2  30370  filbcmb  30397  fdc  30404  fdc1  30405  seqpo  30406  incsequz  30407  incsequz2  30408  metf1o  30414  lmclim2  30417  geomcau  30418  isbnd2  30445  bndss  30448  ismtybndlem  30468  heibor1lem  30471  rrncmslem  30494  rrnequiv  30497  exidreslem  30505  ghomco  30511  isdrngo3  30528  rngoisocnv  30550  isidlc  30578  idlnegcl  30585  divrngidl  30591  intidl  30592  unichnidl  30594  keridl  30595  igenmin  30627  prnc  30630  ispridlc  30633  prter3  30789  lsmfgcl  31186  kercvrlsm  31195  unxpwdom3  31207  hbt  31247  cntzsdrg  31319  cvgdvgrat  31362  lcmgcdlem  31380  lcmdvds  31382  climinf  31778  clim2f  31808  clim2cf  31822  clim0cf  31826  mgmhmpropd  32791  mgmhmima  32808  ovmpt2rdxf  33128  cotsqcscsq  33492  aacllem  33550  glbconxN  35515  atltcvr  35572  3dim1  35604  lvolnle3at  35719  linepsubN  35889  osumclN  36104  pexmidALTN  36115  lhpmatb  36168  cdlemg1idlemN  36711  dihlss  37390  dihglblem5aN  37432  dihatlat  37474
  Copyright terms: Public domain W3C validator