Theorem anassrs 467

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anass  468  anass1rs  655  anabss5  668  anabss7  673  mpanr1  703  pm2.61ddan  813  pm2.61dda  814  pm2.61da2ne  3017  ralimdvva  3180  reximdvva  3181  2ralbidva  3195  2rexbidva  3196  2ralbida  3256  spcimgft  3500  copsexgw  5433  copsexg  5434  pofun  5545  imainss  6106  fvmptdf  6941  eqfnfv2  6971  fnex  7157  f1elima  7203  fliftfun  7252  isores2  7273  f1oiso  7291  ovmpodxf  7502  sorpssuni  7671  sorpssint  7672  tfindsg2  7798  2ndconst  8037  poxp2  8079  sexp3  8089  poseq  8094  oalim  8453  omlim  8454  oaass  8482  omlimcl  8499  omass  8501  oelim2  8516  oeoa  8518  oeoelem  8519  nnaass  8543  omabs  8572  eroveu  8742  sbthlem4  9010  fimaxg  9178  fisupg  9179  fofinf1o  9223  fiming  9391  fiinfg  9392  ordtypelem7  9417  hartogs  9437  card2on  9447  unwdomg  9477  wemapwe  9594  frmin  9649  dfac5  10027  cfsmolem  10168  isf32lem2  10252  ttukeylem6  10412  ondomon  10461  alephreg  10480  ltexprlem6  10939  recexsrlem  11001  wloglei  11656  recextlem2  11755  fimaxre  12073  creur  12126  uz11  12763  xrmaxeq  13080  xrmineq  13081  xaddf  13125  xaddass  13150  xleadd1a  13154  xlt2add  13161  xmullem  13165  xmulgt0  13184  xmulasslem3  13187  xlemul1a  13189  xadddilem  13195  fzrevral  13514  seqcaopr2  13947  expnlbnd2  14143  faclbnd4lem4  14205  hashgt23el  14333  rtrclreclem3  14969  rtrclreclem4  14970  relexpindlem  14972  rtrclind  14974  shftlem  14977  01sqrex  15158  cau3lem  15264  limsupbnd2  15392  clim2  15413  clim2c  15414  clim0c  15416  rlimresb  15474  2clim  15481  climabs0  15494  climcn1  15501  climcn2  15502  o1rlimmul  15528  climsqz  15550  climsqz2  15551  rlimsqzlem  15558  lo1le  15561  climsup  15579  caucvgrlem2  15584  iseralt  15594  summolem2  15625  fsum2dlem  15679  cvgcmp  15725  cvgcmpce  15727  climfsum  15729  fsumiun  15730  geomulcvg  15785  mertenslem2  15794  mertens  15795  prodfn0  15803  prodfrec  15804  zprod  15846  fprodeq0  15884  fprodn0  15888  fprod2dlem  15889  smu01lem  16398  gcdcllem1  16412  dvdssq  16480  lcmdvds  16521  coprmdvds2  16567  pclem  16752  pcge0  16776  pcgcd1  16791  prmpwdvds  16818  1arithlem4  16840  4sqlem18  16876  vdwlem10  16904  vdwlem11  16905  ramval  16922  ramub1lem2  16941  ramcl  16943  imasaddfnlem  17434  imasaddflem  17436  imasvscafn  17443  imasleval  17447  ismon2  17643  isepi2  17650  issubc3  17758  cofucl  17797  setcmon  17996  setcepi  17997  ipodrsfi  18447  ipodrsima  18449  isacs3lem  18450  grpidpropd  18572  grprida  18585  gsumpropd2lem  18589  mgmhmpropd  18608  mgmhmima  18625  mhmpropd  18702  mhmimalem  18734  grplcan  18915  dfgrp3lem  18953  mulgdirlem  19020  subgmulg  19055  issubg4  19060  subgint  19065  ssnmz  19080  cycsubgcl  19120  gastacl  19223  orbsta  19227  cntzsubg  19253  galactghm  19318  odmulg  19470  odbezout  19472  sylow3lem2  19542  lsmsubm  19567  efgsfo  19653  mulgmhm  19741  mulgghm  19742  gsumval3  19821  gsumcllem  19822  gsumpt  19876  gsum2d  19886  gsum2d2  19888  prdsgsum  19895  subgdmdprd  19950  dprd2d2  19960  ablfac1eu  19989  rngpropd  20094  srglmhm  20141  srgrmhm  20142  ringpropd  20208  ringlghm  20232  dvdsrpropd  20336  rhmimasubrnglem  20482  cntzsdrg  20719  abvpropd  20752  islmodd  20801  lmodprop2d  20859  lsssubg  20892  lsspropd  20953  lmhmima  20983  lidlsubg  21162  phlpropd  21594  frlmsslsp  21735  lindfmm  21766  islindf4  21777  assapropd  21811  asclpropd  21836  psrass1lem  21871  mplcoe1  21973  mplcoe5  21976  mplind  22006  evlslem2  22015  evlsval  22022  coe1tmmul2  22191  mamuass  22318  mavmulass  22465  mdetuni0  22537  mdetmul  22539  cpmatacl  22632  cpmadugsumfi  22793  cpmadumatpolylem1  22797  cpmadumatpolylem2  22798  cpmadumatpoly  22799  cayhamlem4  22804  neips  23029  neindisj  23033  ordtrest2lem  23119  lmbrf  23176  lmss  23214  isreg2  23293  lmmo  23296  hauscmplem  23322  bwth  23326  2ndcomap  23374  1stcelcls  23377  restlly  23399  islly2  23400  cldllycmp  23411  comppfsc  23448  1stckgenlem  23469  txbas  23483  txbasval  23522  tx1cn  23525  ptpjopn  23528  ptcnp  23538  txnlly  23553  txlm  23564  xkococn  23576  fgabs  23795  fmfnfmlem4  23873  flimcf  23898  hauspwpwf1  23903  fclsbas  23937  fclscf  23941  flimfnfcls  23944  ghmcnp  24031  tsmsxp  24071  isxmet2d  24243  elmopn2  24361  mopni3  24410  blsscls2  24420  metequiv2  24426  metss2lem  24427  met2ndci  24438  metrest  24440  metcnp  24457  metcnp2  24458  metcnpi3  24462  txmetcnp  24463  nmolb2d  24634  xrge0tsms  24751  metdsre  24770  metnrmlem3  24778  fsumcn  24789  elcncf2  24811  mulc1cncf  24826  cncfco  24828  cncfmet  24830  bndth  24885  evth  24886  copco  24946  pcopt2  24951  pcoass  24952  pcorevlem  24954  lmmcvg  25189  lmmbrf  25190  iscau4  25207  iscauf  25208  cmetcaulem  25216  iscmet3lem3  25218  iscmet3lem1  25219  causs  25226  equivcfil  25227  lmclim  25231  caubl  25236  caublcls  25237  bcth3  25259  ivthle  25385  ivthle2  25386  ovoliunlem1  25431  ovolicc2lem5  25450  volsuplem  25484  uniioombllem6  25517  dyaddisjlem  25524  dyadmax  25527  volcn  25535  mbfmulc2lem  25576  ismbf3d  25583  mbfsup  25593  mbfinf  25594  mbflim  25597  i1fmullem  25623  itg2seq  25671  itg2uba  25672  itg2splitlem  25677  itg2split  25678  itg2monolem1  25679  bddiblnc  25771  ditgsplitlem  25789  ellimc2  25806  ellimc3  25808  limcflf  25810  limcmpt  25812  limcco  25822  lhop1lem  25946  dvfsumle  25954  dvfsumleOLD  25955  dvfsumabs  25957  dvfsumrlim  25966  ftc1a  25972  ftc1lem6  25976  mdegmullem  26011  elply2  26129  plypf1  26145  ulmcaulem  26331  ulmcau  26332  ulmss  26334  ulmdvlem3  26339  mtest  26341  itgulm  26345  abelthlem8  26377  abelth  26379  tanord  26475  cxpcn3lem  26685  mcubic  26785  cubic2  26786  dvdsflsumcom  27126  fsumdvdsmul  27133  fsumdvdsmulOLD  27135  lgsdchrval  27293  2sqlem9  27366  rplogsumlem2  27424  rpvmasumlem  27426  dchrvmasumlem1  27434  vmalogdivsum2  27477  logsqvma  27481  selberg  27487  selberg4  27500  pntibndlem3  27531  pntlem3  27548  pntleml  27550  padicabv  27569  padicabvf  27570  padicabvcxp  27571  ostth3  27577  nosupbnd1lem5  27652  noinfbnd1lem5  27667  nocvxminlem  27718  lrrecfr  27887  addsprop  27920  mulsproplem9  28064  mulsproplem12  28067  mulsproplem13  28068  mulsproplem14  28069  mulsprop  28070  slemuld  28078  mulsuniflem  28089  mulsasslem3  28105  axpasch  28921  axcontlem7  28950  axcontlem10  28953  cusgrsize2inds  29434  grpolcan  30512  nvmul0or  30632  nmosetre  30746  blocnilem  30786  blocni  30787  h2hcau  30961  h2hlm  30962  shsel3  31297  chscllem2  31620  homulcl  31741  adjsym  31815  cnvadj  31874  hhcno  31886  hhcnf  31887  lnopl  31896  unoplin  31902  counop  31903  lnfnl  31913  hmoplin  31924  hmopm  32003  nmcexi  32008  lnconi  32015  riesz3i  32044  leopmuli  32115  leopmul  32116  hstle  32212  mdsl0  32292  mdslmd1lem2  32308  atcvatlem  32367  chirredi  32376  cdj1i  32415  sbc2iedf  32446  foresf1o  32486  suppovss  32666  isoun  32687  difioo  32769  swrdf1  32944  xrge0tsmsd  33049  cycpmrn  33119  ressply1invg  33539  ply1unit  33545  fedgmullem2  33664  pstmxmet  33931  ordtrest2NEWlem  33956  esum2dlem  34126  esum2d  34127  dya2icoseg2  34312  eulerpartlemgc  34396  eulerpartlemgh  34412  eulerpartlemgs2  34414  ballotlemimin  34540  signstfvneq0  34606  hgt750lemb  34690  connpconn  35300  cvmliftmolem2  35347  cvmliftlem6  35355  cvmliftlem8  35357  cvmlift2lem12  35379  elmrsubrn  35585  dfon2lem6  35851  ifscgr  36109  brsegle  36173  neibastop2lem  36425  bj-elabd2ALT  36990  bj-ismooredr2  37175  curf  37658  finixpnum  37665  fin2solem  37666  fin2so  37667  lindsenlbs  37675  matunitlindflem1  37676  matunitlindflem2  37677  matunitlindf  37678  poimirlem3  37683  poimirlem4  37684  poimirlem6  37686  poimirlem7  37687  poimirlem14  37694  poimirlem16  37696  poimirlem19  37699  poimirlem22  37702  poimirlem28  37708  poimirlem29  37709  poimirlem30  37710  poimir  37713  heicant  37715  itg2gt0cn  37735  ftc1cnnc  37752  ftc1anclem5  37757  ftc1anclem6  37758  ftc1anclem7  37759  ftc1anc  37761  cover2  37775  filbcmb  37800  fdc  37805  fdc1  37806  seqpo  37807  incsequz  37808  incsequz2  37809  metf1o  37815  lmclim2  37818  geomcau  37819  isbnd2  37843  bndss  37846  ismtybndlem  37866  heibor1lem  37869  rrncmslem  37892  rrnequiv  37895  exidreslem  37937  ghomco  37951  isdrngo3  38019  rngoisocnv  38041  isidlc  38075  idlnegcl  38082  divrngidl  38088  intidl  38089  unichnidl  38091  keridl  38092  igenmin  38124  prnc  38127  ispridlc  38130  erimeq2  38796  prter3  39001  glbconxN  39497  atltcvr  39554  3dim1  39586  lvolnle3at  39701  linepsubN  39871  osumclN  40086  pexmidALTN  40097  lhpmatb  40150  cdlemg1idlemN  40691  dihlss  41369  dihglblem5aN  41411  dihatlat  41453  aks6d1c1p1  42220  aks6d1c5lem1  42249  unitscyglem4  42311  f1o2d2  42351  pwsgprod  42662  selvvvval  42703  fsuppind  42708  fsuppssindlem1  42709  prjspertr  42723  prjspreln0  42727  lsmfgcl  43191  kercvrlsm  43200  unxpwdom3  43212  hbt  43247  oa0suclim  43392  om0suclim  43393  oe0suclim  43394  naddcnff  43479  cvgdvgrat  44430  climinf  45730  clim2f  45758  clim2cf  45772  clim0cf  45776  clim2f2  45792  fmtnofac2lem  47692  ovmpordxf  48463  oppcthinendcALT  49566  cotsqcscsq  49887  aacllem  49926