Theorem anassrs 461

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
anassrs.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
anassrs	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem anassrs

Step	Hyp	Ref	Expression
1		anassrs.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 413	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 410	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  anass  462  anass1rs  645  anabss5  658  anabss7  663  mpanr1  694  pm2.61ddan  848  pm2.61dda  849  pm2.61da2ne  3087  ralimdvva  3173  2ralbida  3196  2ralbidva  3197  reximdvva  3228  2rexbidva  3266  copsexg  5178  pofun  5282  imainss  5793  eqfnfv2  6566  fnex  6742  f1elima  6780  fliftfun  6822  isores2  6843  f1oiso  6861  ovmpt2dxf  7051  grpridd  7139  sorpssuni  7211  sorpssint  7212  tfindsg2  7327  2ndconst  7535  oalim  7884  omlim  7885  oaass  7913  omlimcl  7930  omass  7932  oelim2  7947  oeoa  7949  oeoelem  7950  nnaass  7974  omabs  7999  eroveu  8113  sbthlem4  8348  fimaxg  8482  fisupg  8483  fofinf1o  8516  fiming  8679  fiinfg  8680  ordtypelem7  8705  hartogs  8725  card2on  8735  unwdomg  8765  wemapwe  8878  dfac5  9271  cfsmolem  9414  isf32lem2  9498  ttukeylem6  9658  ondomon  9707  alephreg  9726  ltexprlem6  10185  recexsrlem  10247  wloglei  10891  recextlem2  10990  fimaxre  11305  creur  11351  uz11  11998  xrmaxeq  12305  xrmineq  12306  xaddf  12350  xaddass  12374  xleadd1a  12378  xlt2add  12385  xmullem  12389  xmulgt0  12408  xmulasslem3  12411  xlemul1a  12413  xadddilem  12419  fzrevral  12726  seqcaopr2  13138  expnlbnd2  13296  faclbnd4lem4  13383  rtrclreclem3  14184  rtrclreclem4  14185  relexpindlem  14187  rtrclind  14189  shftlem  14192  01sqrex  14374  cau3lem  14478  limsupbnd2  14598  clim2  14619  clim2c  14620  clim0c  14622  rlimresb  14680  2clim  14687  climabs0  14700  climcn1  14706  climcn2  14707  o1rlimmul  14733  climsqz  14755  climsqz2  14756  rlimsqzlem  14763  lo1le  14766  climsup  14784  caucvgrlem2  14789  iseralt  14799  summolem2  14831  fsum2dlem  14883  cvgcmp  14929  cvgcmpce  14931  climfsum  14933  fsumiun  14934  geomulcvg  14988  mertenslem2  14997  mertens  14998  prodfn0  15006  prodfrec  15007  zprod  15047  fprodeq0  15085  fprodn0  15089  fprod2dlem  15090  smu01lem  15587  gcdcllem1  15601  gcdmultiplez  15650  dvdssq  15660  lcmdvds  15701  coprmdvds2  15747  pclem  15921  pcge0  15944  pcgcd1  15959  prmpwdvds  15986  1arithlem4  16008  4sqlem18  16044  vdwlem10  16072  vdwlem11  16073  ramval  16090  ramub1lem2  16109  ramcl  16111  imasaddfnlem  16548  imasaddflem  16550  imasvscafn  16557  imasleval  16561  ismon2  16753  isepi2  16760  issubc3  16868  cofucl  16907  setcmon  17096  setcepi  17097  ipodrsfi  17523  ipodrsima  17525  isacs3lem  17526  grpidpropd  17621  gsumpropd2lem  17633  mhmpropd  17701  mhmima  17723  gsumccat  17738  grplcan  17838  dfgrp3lem  17874  mulgdirlem  17931  subgmulg  17966  issubg4  17971  subgint  17976  cycsubgcl  17978  ssnmz  17994  gastacl  18099  orbsta  18103  cntzsubg  18126  galactghm  18180  odmulg  18331  odbezout  18333  sylow3lem2  18401  lsmsubm  18426  efgsfo  18511  mulgmhm  18593  mulgghm  18594  gsumval3  18668  gsumcllem  18669  gsumpt  18721  gsum2d  18731  gsum2d2  18733  prdsgsum  18737  subgdmdprd  18794  dprd2d2  18804  ablfac1eu  18833  srglmhm  18896  srgrmhm  18897  ringpropd  18943  ringlghm  18965  dvdsrpropd  19057  abvpropd  19205  islmodd  19232  lmodprop2d  19288  lsssubg  19323  lsspropd  19383  lmhmima  19413  lidlsubg  19583  assapropd  19695  asclpropd  19714  psrass1lem  19745  mplcoe1  19833  mplcoe5  19836  mplind  19869  evlslem2  19879  evlsval  19886  coe1tmmul2  20013  phlpropd  20369  frlmsslsp  20509  lindfmm  20540  islindf4  20551  mamuass  20582  mavmulass  20730  mdetuni0  20802  mdetmul  20804  cpmatacl  20898  cpmadugsumfi  21059  cpmadumatpolylem1  21063  cpmadumatpolylem2  21064  cpmadumatpoly  21065  cayhamlem4  21070  neips  21295  neindisj  21299  ordtrest2lem  21385  lmbrf  21442  lmss  21480  isreg2  21559  lmmo  21562  hauscmplem  21587  bwth  21591  2ndcomap  21639  1stcelcls  21642  restlly  21664  islly2  21665  cldllycmp  21676  comppfsc  21713  1stckgenlem  21734  txbas  21748  txbasval  21787  tx1cn  21790  ptpjopn  21793  ptcnp  21803  txnlly  21818  txlm  21829  xkococn  21841  fgabs  22060  fmfnfmlem4  22138  flimcf  22163  hauspwpwf1  22168  fclsbas  22202  fclscf  22206  flimfnfcls  22209  ghmcnp  22295  tsmsxp  22335  isxmet2d  22509  elmopn2  22627  mopni3  22676  blsscls2  22686  metequiv2  22692  metss2lem  22693  met2ndci  22704  metrest  22706  metcnp  22723  metcnp2  22724  metcnpi3  22728  txmetcnp  22729  nmolb2d  22899  xrge0tsms  23014  metdsre  23033  metnrmlem3  23041  fsumcn  23050  elcncf2  23070  mulc1cncf  23085  cncfco  23087  cncfmet  23088  bndth  23134  evth  23135  copco  23194  pcopt2  23199  pcoass  23200  pcorevlem  23202  lmmcvg  23436  lmmbrf  23437  iscau4  23454  iscauf  23455  cmetcaulem  23463  iscmet3lem3  23465  iscmet3lem1  23466  causs  23473  equivcfil  23474  lmclim  23478  caubl  23483  caublcls  23484  bcth3  23506  ivthle  23629  ivthle2  23630  ovoliunlem1  23675  ovolicc2lem5  23694  volsuplem  23728  uniioombllem6  23761  dyaddisjlem  23768  dyadmax  23771  volcn  23779  mbfmulc2lem  23820  ismbf3d  23827  mbfsup  23837  mbfinf  23838  mbflim  23841  i1fmullem  23867  itg2seq  23915  itg2uba  23916  itg2splitlem  23921  itg2split  23922  itg2monolem1  23923  ditgsplitlem  24030  ellimc2  24047  ellimc3  24049  limcflf  24051  limcmpt  24053  limcco  24063  lhop1lem  24182  dvfsumle  24190  dvfsumabs  24192  dvfsumrlim  24200  ftc1a  24206  ftc1lem6  24210  mdegmullem  24244  elply2  24358  plypf1  24374  ulmcaulem  24554  ulmcau  24555  ulmss  24557  ulmdvlem3  24562  mtest  24564  itgulm  24568  abelthlem8  24599  abelth  24601  tanord  24691  cxpcn3lem  24897  mcubic  24994  cubic2  24995  dvdsflsumcom  25334  fsumdvdsmul  25341  lgsdchrval  25499  2sqlem9  25572  rplogsumlem2  25594  rpvmasumlem  25596  dchrvmasumlem1  25604  vmalogdivsum2  25647  logsqvma  25651  selberg  25657  selberg4  25670  pntibndlem3  25701  pntlem3  25718  pntleml  25720  padicabv  25739  padicabvf  25740  padicabvcxp  25741  ostth3  25747  axpasch  26247  axcontlem7  26276  axcontlem10  26279  cusgrsize2inds  26758  grpolcan  27936  nvmul0or  28056  nmosetre  28170  blocnilem  28210  blocni  28211  h2hcau  28387  h2hlm  28388  shsel3  28725  chscllem2  29048  homulcl  29169  adjsym  29243  cnvadj  29302  hhcno  29314  hhcnf  29315  lnopl  29324  unoplin  29330  counop  29331  lnfnl  29341  hmoplin  29352  hmopm  29431  nmcexi  29436  lnconi  29443  riesz3i  29472  leopmuli  29543  leopmul  29544  hstle  29640  mdsl0  29720  mdslmd1lem2  29736  atcvatlem  29795  chirredi  29804  cdj1i  29843  foresf1o  29887  isoun  30023  difioo  30087  xrge0tsmsd  30326  pstmxmet  30481  ordtrest2NEWlem  30509  esum2dlem  30695  esum2d  30696  dya2icoseg2  30881  eulerpartlemgc  30965  eulerpartlemgh  30981  eulerpartlemgs2  30983  ballotlemimin  31109  signstfvneq0  31193  hgt750lemb  31279  connpconn  31759  cvmliftmolem2  31806  cvmliftlem6  31814  cvmliftlem8  31816  cvmlift2lem12  31838  elmrsubrn  31959  elintfv  32199  dfon2lem6  32226  poseq  32287  nosupbnd1lem5  32392  nocvxminlem  32427  ifscgr  32685  brsegle  32749  neibastop2lem  32888  curf  33929  finixpnum  33936  fin2solem  33937  fin2so  33938  lindsenlbs  33947  matunitlindflem1  33948  matunitlindflem2  33949  matunitlindf  33950  poimirlem3  33955  poimirlem4  33956  poimirlem6  33958  poimirlem7  33959  poimirlem14  33966  poimirlem16  33968  poimirlem19  33971  poimirlem22  33974  poimirlem28  33980  poimirlem29  33981  poimirlem30  33982  poimir  33985  heicant  33987  itg2gt0cn  34007  bddiblnc  34022  ftc1cnnc  34026  ftc1anclem5  34031  ftc1anclem6  34032  ftc1anclem7  34033  ftc1anc  34035  cover2  34050  filbcmb  34077  fdc  34082  fdc1  34083  seqpo  34084  incsequz  34085  incsequz2  34086  metf1o  34092  lmclim2  34095  geomcau  34096  isbnd2  34123  bndss  34126  ismtybndlem  34146  heibor1lem  34149  rrncmslem  34172  rrnequiv  34175  exidreslem  34217  ghomco  34231  isdrngo3  34299  rngoisocnv  34321  isidlc  34355  idlnegcl  34362  divrngidl  34368  intidl  34369  unichnidl  34371  keridl  34372  igenmin  34404  prnc  34407  ispridlc  34410  prter3  34956  glbconxN  35452  atltcvr  35509  3dim1  35541  lvolnle3at  35656  linepsubN  35826  osumclN  36041  pexmidALTN  36052  lhpmatb  36105  cdlemg1idlemN  36646  dihlss  37324  dihglblem5aN  37366  dihatlat  37408  lsmfgcl  38486  kercvrlsm  38495  unxpwdom3  38507  hbt  38542  cntzsdrg  38614  cvgdvgrat  39351  climinf  40631  clim2f  40661  clim2cf  40675  clim0cf  40679  clim2f2  40695  fmtnofac2lem  42328  isomuspgrlem2d  42567  mgmhmpropd  42650  mgmhmima  42667  ovmpt2rdxf  42982  cotsqcscsq  43415  aacllem  43457