Theorem anassrs 472

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 425	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 422	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  anass  473  anass1rs  667  anabss5  680  anabss7  685  mpanr1  715  pm2.61ddan  825  pm2.61dda  826  pm2.61da2ne  3045  ralimdvva  3211  reximdvva  3212  2ralbidva  3226  2rexbidva  3227  2ralbida  3287  spcimgft  3514  copsexgwOLD  5472  copsexg  5473  pofun  5586  imainss  6150  fvmptdf  6996  eqfnfv2  7026  fnex  7215  f1elima  7261  fliftfun  7310  isores2  7331  f1oiso  7349  ovmpodxf  7562  sorpssuni  7731  sorpssint  7732  tfindsg2  7856  2ndconst  8094  mpof1o2d  8119  poxp2  8137  sexp3  8147  poseq  8152  oalim  8515  omlim  8516  oaass  8544  omlimcl  8561  omass  8563  oelim2  8579  oeoa  8581  oeoelem  8582  nnaass  8606  omabs  8635  eroveu  8808  sbthlem4  9076  fimaxg  9245  fisupg  9246  fofinf1o  9287  fiming  9458  fiinfg  9459  ordtypelem7  9484  hartogs  9504  card2on  9514  unwdomg  9544  wemapwe  9664  frmin  9719  dfac5  10119  cfsmolem  10260  isf32lem2  10344  ttukeylem6  10504  ondomon  10553  alephreg  10573  ltexprlem6  11032  recexsrlem  11094  wloglei  11752  recextlem2  11851  fimaxre  12165  creur  12218  uz11  12893  xrmaxeq  13211  xrmineq  13212  xaddf  13256  xaddass  13281  xleadd1a  13285  xlt2add  13292  xmullem  13296  xmulgt0  13315  xmulasslem3  13318  xlemul1a  13320  xadddilem  13326  fzrevral  13647  seqcaopr2  14081  expnlbnd2  14277  faclbnd4lem4  14339  hashgt23el  14468  rtrclreclem3  15104  rtrclreclem4  15105  relexpindlem  15107  rtrclind  15109  shftlem  15112  01sqrex  15307  cau3lem  15413  limsupbnd2  15541  clim2  15562  clim2c  15563  clim0c  15565  rlimresb  15623  2clim  15630  climabs0  15643  climcn1  15650  climcn2  15651  o1rlimmul  15677  climsqz  15699  climsqz2  15700  rlimsqzlem  15707  lo1le  15710  climsup  15728  caucvgrlem2  15733  iseralt  15743  summolem2  15774  fsum2dlem  15828  cvgcmp  15875  cvgcmpce  15877  climfsum  15879  fsumiun  15880  geomulcvg  15937  mertenslem2  15946  mertens  15947  prodfn0  15955  prodfrec  15956  zprod  15998  fprodeq0  16036  fprodn0  16040  fprod2dlem  16041  smu01lem  16549  gcdcllem1  16563  dvdssq  16631  lcmdvds  16672  coprmdvds2  16718  pclem  16904  pcge0  16928  pcgcd1  16943  prmpwdvds  16970  1arithlem4  16992  4sqlem18  17028  vdwlem10  17056  vdwlem11  17057  ramval  17074  ramub1lem2  17093  ramcl  17095  imasaddfnlem  17588  imasaddflem  17590  imasvscafn  17597  imasleval  17601  ismon2  17797  isepi2  17804  issubc3  17912  cofucl  17951  setcmon  18150  setcepi  18151  ipodrsfi  18601  ipodrsima  18603  isacs3lem  18604  grpidpropd  18726  grprida  18739  gsumpropd2lem  18743  mgmhmpropd  18762  mgmhmima  18779  mhmpropd  18856  mhmimalem  18889  grplcan  19073  dfgrp3lem  19110  mulgdirlem  19177  subgmulg  19213  issubg4  19218  subgint  19223  ssnmz  19238  cycsubgcl  19283  gastacl  19385  orbsta  19389  cntzsubg  19415  galactghm  19480  odmulg  19632  odbezout  19634  sylow3lem2  19704  lsmsubm  19729  efgsfo  19815  mulgmhm  19903  mulgghm  19904  gsumval3  19983  gsumcllem  19984  gsumpt  20038  gsum2d  20048  gsum2d2  20050  prdsgsum  20057  subgdmdprd  20112  dprd2d2  20122  ablfac1eu  20151  rngpropd  20258  srglmhm  20309  srgrmhm  20310  ringpropd  20378  ringlghm  20402  pwsgprod  20418  dvdsrpropd  20505  rhmimasubrnglem  20675  isdrng5  20865  cntzsdrg  20916  abvpropd  20949  islmodd  20998  lmodprop2d  21056  lsssubg  21089  lsspropd  21149  lmhmima  21179  lidlsubg  21359  phlpropd  21816  frlmsslsp  21957  lindfmm  21988  islindf4  21999  assapropd  22032  asclpropd  22058  psrass1lem  22094  mplcoe1  22199  mplcoe5  22202  mplind  22232  evlslem2  22241  evlsval  22248  selvvvval  22304  coe1tmmul2  22448  mamuass  22570  mavmulass  22717  mdetuni0  22789  mdetmul  22791  cpmatacl  22884  cpmadugsumfi  23045  cpmadumatpolylem1  23049  cpmadumatpolylem2  23050  cpmadumatpoly  23051  cayhamlem4  23056  neips  23281  neindisj  23285  ordtrest2lem  23371  lmbrf  23428  lmss  23466  isreg2  23545  lmmo  23548  hauscmplem  23574  bwth  23578  2ndcomap  23626  1stcelcls  23629  restlly  23651  islly2  23652  cldllycmp  23663  comppfsc  23700  1stckgenlem  23721  txbas  23735  txbasval  23774  tx1cn  23777  ptpjopn  23780  ptcnp  23790  txnlly  23805  txlm  23816  xkococn  23828  fgabs  24047  fmfnfmlem4  24125  flimcf  24150  hauspwpwf1  24155  fclsbas  24189  fclscf  24193  flimfnfcls  24196  ghmcnp  24283  tsmsxp  24323  isxmet2d  24495  elmopn2  24613  mopni3  24662  blsscls2  24672  metequiv2  24678  metss2lem  24679  met2ndci  24690  metrest  24692  metcnp  24709  metcnp2  24710  metcnpi3  24714  txmetcnp  24715  nmolb2d  24886  xrge0tsms  25003  metdsre  25022  metnrmlem3  25030  fsumcn  25040  elcncf2  25060  mulc1cncf  25075  cncfco  25077  cncfmet  25079  bndth  25128  evth  25129  copco  25188  pcopt2  25193  pcoass  25194  pcorevlem  25196  lmmcvg  25431  lmmbrf  25432  iscau4  25449  iscauf  25450  cmetcaulem  25458  iscmet3lem3  25460  iscmet3lem1  25461  causs  25468  equivcfil  25469  lmclim  25473  caubl  25478  caublcls  25479  bcth3  25501  ivthle  25626  ivthle2  25627  ovoliunlem1  25672  ovolicc2lem5  25691  volsuplem  25725  uniioombllem6  25758  dyaddisjlem  25765  dyadmax  25768  volcn  25776  mbfmulc2lem  25817  ismbf3d  25824  mbfsup  25834  mbfinf  25835  mbflim  25838  i1fmullem  25864  itg2seq  25912  itg2uba  25913  itg2splitlem  25918  itg2split  25919  itg2monolem1  25920  bddiblnc  26012  ditgsplitlem  26030  ellimc2  26047  ellimc3  26049  limcflf  26051  limcmpt  26053  limcco  26063  lhop1lem  26183  dvfsumle  26191  dvfsumabs  26193  dvfsumrlim  26201  ftc1a  26207  ftc1lem6  26211  mdegmullem  26246  elply2  26364  plypf1  26380  ulmcaulem  26568  ulmcau  26569  ulmss  26571  ulmdvlem3  26576  mtest  26578  itgulm  26582  abelthlem8  26613  abelth  26615  tanord  26714  cxpcn3lem  26923  mcubic  27023  cubic2  27024  dvdsflsumcom  27363  fsumdvdsmul  27370  lgsdchrval  27529  2sqlem9  27602  rplogsumlem2  27660  rpvmasumlem  27662  dchrvmasumlem1  27670  vmalogdivsum2  27713  logsqvma  27717  selberg  27723  selberg4  27736  pntibndlem3  27767  pntlem3  27784  pntleml  27786  padicabv  27805  padicabvf  27806  padicabvcxp  27807  ostth3  27813  nosupbnd1lem5  27887  noinfbnd1lem5  27902  nocvxminlem  27958  lrrecfr  28147  addsprop  28180  mulsproplem9  28328  mulsproplem12  28331  mulsproplem13  28332  mulsproplem14  28333  mulsprop  28334  lemulsd  28342  mulsuniflem  28353  mulsasslem3  28369  axpasch  29302  axcontlem7  29331  axcontlem10  29334  cusgrsize2inds  29814  grpolcan  30893  nvmul0or  31013  nmosetre  31127  blocnilem  31167  blocni  31168  h2hcau  31342  h2hlm  31343  shsel3  31678  chscllem2  32001  homulcl  32122  adjsym  32196  cnvadj  32255  hhcno  32267  hhcnf  32268  lnopl  32277  unoplin  32283  counop  32284  lnfnl  32294  hmoplin  32305  hmopm  32384  nmcexi  32389  lnconi  32396  riesz3i  32425  leopmuli  32496  leopmul  32497  hstle  32593  mdsl0  32673  mdslmd1lem2  32689  atcvatlem  32748  chirredi  32757  cdj1i  32796  sbc2iedf  32823  foresf1o  32861  suppovss  33037  isoun  33058  difioo  33138  swrdf1  33285  xrge0tsmsd  33402  cycpmrn  33472  ressply1invg  33868  ply1unit  33874  fedgmullem2  34029  pstmxmet  34296  ordtrest2NEWlem  34321  esum2dlem  34491  esum2d  34492  dya2icoseg2  34677  eulerpartlemgc  34761  eulerpartlemgh  34777  eulerpartlemgs2  34779  ballotlemimin  34905  signstfvneq0  34968  hgt750lemb  35052  connpconn  35735  cvmliftmolem2  35782  cvmliftlem6  35790  cvmliftlem8  35792  cvmlift2lem12  35814  elmrsubrn  36020  dfon2lem6  36286  ifscgr  36544  brsegle  36608  neibastop2lem  36899  bj-elabd2ALT  37589  bj-ismooredr2  37780  curf  38277  finixpnum  38284  fin2solem  38285  fin2so  38286  lindsenlbs  38294  matunitlindflem1  38295  matunitlindflem2  38296  matunitlindf  38297  poimirlem3  38302  poimirlem4  38303  poimirlem6  38305  poimirlem7  38306  poimirlem14  38313  poimirlem16  38315  poimirlem19  38318  poimirlem22  38321  poimirlem28  38327  poimirlem29  38328  poimirlem30  38329  poimir  38332  heicant  38334  itg2gt0cn  38354  ftc1cnnc  38371  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anc  38380  cover2  38394  filbcmb  38419  fdc  38424  fdc1  38425  seqpo  38426  incsequz  38427  incsequz2  38428  metf1o  38434  lmclim2  38437  geomcau  38438  isbnd2  38462  bndss  38465  ismtybndlem  38485  heibor1lem  38488  rrncmslem  38511  rrnequiv  38514  exidreslem  38556  ghomco  38570  isdrngo3  38638  rngoisocnv  38660  isidlc  38694  idlnegcl  38701  divrngidl  38707  intidl  38708  unichnidl  38710  keridl  38711  igenmin  38743  prnc  38746  ispridlc  38749  erimeq2  39440  prter3  39684  glbconxN  40180  atltcvr  40237  3dim1  40269  lvolnle3at  40384  linepsubN  40554  osumclN  40769  pexmidALTN  40780  lhpmatb  40833  cdlemg1idlemN  41374  dihlss  42052  dihglblem5aN  42094  dihatlat  42136  aks6d1c1p1  42902  aks6d1c5lem1  42931  unitscyglem4  42993  fsuppind  43350  fsuppssindlem1  43351  prjspertr  43365  prjspreln0  43369  lsmfgcl  43829  kercvrlsm  43838  unxpwdom3  43850  hbt  43885  oa0suclim  44030  om0suclim  44031  oe0suclim  44032  naddcnff  44117  cvgdvgrat  45051  climinf  46350  clim2f  46378  clim2cf  46392  clim0cf  46396  clim2f2  46412  fmtnofac2lem  48348  ovmpordxf  49147  oppcthinendcALT  50247  cotsqcscsq  50568  aacllem  50649