Theorem anassrs 473

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

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

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 402

This theorem is used by:  anass  474  anass1rs  668  anabss5  681  anabss7  686  mpanr1  716  pm2.61ddan  826  pm2.61dda  827  pm2.61da2ne  3047  ralimdvva  3213  reximdvva  3214  2ralbidva  3228  2rexbidva  3229  2ralbida  3289  spcimgft  3514  copsexgwOLD  5466  copsexg  5467  pofun  5582  imainss  6157  coass  6285  fvmptdf  7026  eqfnfv2  7056  fnex  7249  f1elima  7293  fliftfun  7346  isores2  7367  f1oiso  7385  ovmpodxf  7597  sorpssuni  7775  sorpssint  7776  tfindsg2  7900  2ndconst  8142  mpof1o2d  8167  poxp2  8190  sexp3  8200  poseq  8205  oalim  8571  omlim  8572  oaass  8600  omlimcl  8617  omass  8619  oelim2  8635  oeoa  8637  oeoelem  8638  nnaass  8662  omabs  8691  eroveu  8864  curf  8921  sbthlem4  9140  fimaxg  9309  fisupg  9310  fofinf1o  9352  fiming  9522  fiinfg  9523  ordtypelem7  9548  hartogs  9568  card2on  9578  unwdomg  9608  wemapwe  9728  frmin  9783  dfac5  10237  cfsmolem  10378  isf32lem2  10462  ttukeylem6  10622  ondomon  10677  alephreg  10697  ltexprlem6  11156  recexsrlem  11218  wloglei  11878  recextlem2  11977  fimaxre  12291  creur  12344  uz11  13020  xrmaxeq  13339  xrmineq  13340  xaddf  13384  xaddass  13409  xleadd1a  13413  xlt2add  13420  xmullem  13424  xmulgt0  13443  xmulasslem3  13446  xlemul1a  13448  xadddilem  13454  fzrevral  13776  seqcaopr2  14211  expnlbnd2  14408  faclbnd4lem4  14470  hashgt23el  14599  swrdf1  14830  rtrclreclem3  15245  rtrclreclem4  15246  relexpindlem  15248  rtrclind  15250  shftlem  15253  01sqrex  15448  cau3lem  15554  limsupbnd2  15682  clim2  15703  clim2c  15704  clim0c  15706  rlimresb  15764  2clim  15771  climabs0  15784  climcn1  15791  climcn2  15792  o1rlimmul  15818  climsqz  15840  climsqz2  15841  rlimsqzlem  15848  lo1le  15851  climsup  15869  caucvgrlem2  15874  iseralt  15884  summolem2  15914  fsum2dlem  15968  cvgcmp  16015  cvgcmpce  16017  climfsum  16019  fsumiun  16020  geomulcvg  16077  mertenslem2  16086  mertens  16087  prodfn0  16095  prodfrec  16096  zprod  16136  fprodeq0  16174  fprodn0  16178  fprod2dlem  16179  smu01lem  16687  gcdcllem1  16701  dvdssq  16774  lcmdvds  16815  coprmdvds2  16861  pclem  17048  pcge0  17072  pcgcd1  17087  prmpwdvds  17114  1arithlem4  17136  4sqlem18  17172  vdwlem10  17200  vdwlem11  17201  ramval  17218  ramub1lem2  17237  ramcl  17239  imasaddfnlem  17732  imasaddflem  17734  imasvscafn  17741  imasleval  17745  ismon2  17941  isepi2  17948  issubc3  18056  cofucl  18095  setcmon  18294  setcepi  18295  ipodrsfi  18745  ipodrsima  18747  isacs3lem  18748  grpidpropd  18874  grprida  18888  gsumpropd2lem  18900  mgmhmpropd  18919  mgmhmima  18936  mhmpropd  19019  mhmimalem  19052  grplcan  19243  dfgrp3lem  19280  mulgdirlem  19347  subgmulg  19383  issubg4  19388  subgint  19393  ssnmz  19408  cycsubgcl  19453  gastacl  19556  orbsta  19560  cntzsubg  19586  galactghm  19651  odmulg  19803  odbezout  19805  sylow3lem2  19875  lsmsubm  19900  efgsfo  19986  mulgmhm  20074  mulgghm  20075  gsumval3  20154  gsumcllem  20155  gsumpt  20209  gsum2d  20219  gsum2d2  20221  prdsgsum  20228  subgdmdprd  20283  dprd2d2  20293  ablfac1eu  20322  rngpropd  20429  srglmhm  20480  srgrmhm  20481  ringpropd  20552  ringlghm  20576  pwsgprod  20592  dvdsrpropd  20679  rhmimasubrnglem  20850  isdrng5  21041  cntzsdrg  21092  abvpropd  21125  islmodd  21174  lmodprop2d  21232  lsssubg  21265  lsspropd  21325  lmhmima  21355  lidlsubg  21535  phlpropd  21994  frlmsslsp  22135  lindfmm  22166  islindf4  22177  lindsenlbs  22190  assapropd  22212  asclpropd  22238  psrass1lem  22274  mplcoe1  22379  mplcoe5  22382  mplind  22412  evlslem2  22421  evlsval  22428  selvvvval  22484  coe1tmmul2  22628  mamuass  22750  mavmulass  22897  mdetuni0  22969  mdetmul  22971  matunitlindflem1  23027  matunitlindflem2  23028  matunitlindf  23029  cpmatacl  23067  cpmadugsumfi  23228  cpmadumatpolylem1  23232  cpmadumatpolylem2  23233  cpmadumatpoly  23234  cayhamlem4  23239  neips  23464  neindisj  23468  ordtrest2lem  23554  lmbrf  23611  lmss  23649  isreg2  23728  lmmo  23731  hauscmplem  23757  bwth  23761  2ndcomap  23810  1stcelcls  23813  restlly  23835  islly2  23836  cldllycmp  23847  comppfsc  23884  1stckgenlem  23905  txbas  23919  txbasval  23958  tx1cn  23961  ptpjopn  23964  ptcnp  23974  txnlly  23989  txlm  24000  xkococn  24012  fgabs  24231  fmfnfmlem4  24309  flimcf  24334  hauspwpwf1  24339  fclsbas  24373  fclscf  24377  flimfnfcls  24380  ghmcnp  24467  tsmsxp  24507  isxmet2d  24679  elmopn2  24797  mopni3  24846  blsscls2  24856  metequiv2  24862  metss2lem  24863  met2ndci  24874  metrest  24876  metcnp  24893  metcnp2  24894  metcnpi3  24898  txmetcnp  24899  nmolb2d  25070  xrge0tsms  25187  metdsre  25206  metnrmlem3  25214  fsumcn  25224  elcncf2  25244  mulc1cncf  25259  cncfco  25261  cncfmet  25263  bndth  25312  evth  25313  copco  25372  pcopt2  25377  pcoass  25378  pcorevlem  25380  lmmcvg  25615  lmmbrf  25616  iscau4  25633  iscauf  25634  cmetcaulem  25642  iscmet3lem3  25644  iscmet3lem1  25645  causs  25652  equivcfil  25653  lmclim  25657  caubl  25662  caublcls  25663  bcth3  25685  ivthle  25810  ivthle2  25811  ovoliunlem1  25856  ovolicc2lem5  25875  volsuplem  25909  uniioombllem6  25942  dyaddisjlem  25949  dyadmax  25952  volcn  25960  mbfmulc2lem  26001  ismbf3d  26008  mbfsup  26018  mbfinf  26019  mbflim  26022  i1fmullem  26048  itg2seq  26096  itg2uba  26097  itg2splitlem  26102  itg2split  26103  itg2monolem1  26104  bddiblnc  26195  ditgsplitlem  26213  ellimc2  26230  ellimc3  26232  limcflf  26234  limcmpt  26236  limcco  26246  lhop1lem  26366  dvfsumle  26374  dvfsumabs  26376  dvfsumrlim  26384  ftc1a  26390  ftc1lem6  26394  mdegmullem  26429  elply2  26547  plypf1  26564  ulmcaulem  26754  ulmcau  26755  ulmss  26757  ulmdvlem3  26762  mtest  26764  itgulm  26768  abelthlem8  26799  abelth  26801  tanord  26899  cxpcn3lem  27108  mcubic  27208  cubic2  27209  dvdsflsumcom  27548  fsumdvdsmul  27555  lgsdchrval  27714  2sqlem9  27787  rplogsumlem2  27845  rpvmasumlem  27847  dchrvmasumlem1  27855  vmalogdivsum2  27898  logsqvma  27902  selberg  27908  selberg4  27921  pntibndlem3  27952  pntlem3  27969  pntleml  27971  padicabv  27990  padicabvf  27991  padicabvcxp  27992  ostth3  27998  nosupbnd1lem5  28102  noinfbnd1lem5  28117  nocvxminlem  28173  lrrecfr  28362  addsprop  28395  mulsproplem9  28543  mulsproplem12  28546  mulsproplem13  28547  mulsproplem14  28548  mulsprop  28549  lemulsd  28557  mulsuniflem  28568  mulsasslem3  28584  axpasch  29552  axcontlem7  29581  axcontlem10  29584  cusgrsize2inds  30067  grpolcan  31165  nvmul0or  31285  nmosetre  31399  blocnilem  31439  blocni  31440  h2hcau  31614  h2hlm  31615  shsel3  31950  chscllem2  32273  homulcl  32394  adjsym  32468  cnvadj  32527  hhcno  32539  hhcnf  32540  lnopl  32549  unoplin  32555  counop  32556  lnfnl  32566  hmoplin  32577  hmopm  32656  nmcexi  32661  lnconi  32668  riesz3i  32697  leopmuli  32768  leopmul  32769  hstle  32865  mdsl0  32945  mdslmd1lem2  32961  atcvatlem  33020  chirredi  33029  cdj1i  33068  sbc2iedf  33137  foresf1o  33175  suppovss  33348  isoun  33369  difioo  33447  xrge0tsmsd  33710  cycpmrn  33780  ressply1invg  34184  ply1unit  34190  fedgmullem2  34345  pstmxmet  34612  ordtrest2NEWlem  34637  esum2dlem  34807  esum2d  34808  dya2icoseg2  34993  eulerpartlemgc  35077  eulerpartlemgh  35093  eulerpartlemgs2  35095  ballotlemimin  35221  signstfvneq0  35284  hgt750lemb  35368  connpconn  36180  cvmliftmolem2  36227  cvmliftlem6  36235  cvmliftlem8  36237  cvmlift2lem12  36259  elmrsubrn  36465  dfon2lem6  36741  ifscgr  37000  brsegle  37064  neibastop2lem  37339  bj-elabd2ALT  38029  bj-ismooredr2  38235  finixpnum  38733  fin2solem  38734  fin2so  38735  poimirlem3  38746  poimirlem4  38747  poimirlem6  38749  poimirlem7  38750  poimirlem14  38757  poimirlem16  38759  poimirlem19  38762  poimirlem22  38765  poimirlem28  38771  poimirlem29  38772  poimirlem30  38773  poimir  38776  heicant  38778  itg2gt0cn  38798  ftc1cnnc  38815  ftc1anclem5  38820  ftc1anclem6  38821  ftc1anclem7  38822  ftc1anc  38824  cover2  38854  filbcmb  38877  fdc  38882  fdc1  38883  seqpo  38884  incsequz  38885  incsequz2  38886  metf1o  38892  lmclim2  38895  geomcau  38896  isbnd2  38920  bndss  38923  ismtybndlem  38943  heibor1lem  38946  rrncmslem  38969  rrnequiv  38972  exidreslem  39014  ghomco  39028  isdrngo3  39096  rngoisocnv  39118  isidlc  39152  idlnegcl  39159  divrngidl  39165  intidl  39166  unichnidl  39168  keridl  39169  igenmin  39201  prnc  39204  ispridlc  39207  erimeq2  39898  prter3  40142  glbconxN  40638  atltcvr  40695  3dim1  40727  lvolnle3at  40842  linepsubN  41012  osumclN  41227  pexmidALTN  41238  lhpmatb  41291  cdlemg1idlemN  41832  dihlss  42510  dihglblem5aN  42552  dihatlat  42594  aks6d1c1p1  43360  aks6d1c5lem1  43389  unitscyglem4  43451  fsuppind  43822  fsuppssindlem1  43823  prjspertr  43837  prjspreln0  43841  lsmfgcl  44280  kercvrlsm  44289  unxpwdom3  44301  hbt  44335  oa0suclim  44480  om0suclim  44481  oe0suclim  44482  naddcnff  44567  cvgdvgrat  45500  climinf  46833  clim2f  46861  clim2cf  46875  clim0cf  46879  clim2f2  46895  fmtnofac2lem  48868  ovmpordxf  49666  oppcthinendcALT  50791  cotsqcscsq  51167  aacllem  51251