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  656  anabss5  669  anabss7  674  mpanr1  704  pm2.61ddan  814  pm2.61dda  815  pm2.61da2ne  3021  ralimdvva  3185  reximdvva  3186  2ralbidva  3200  2rexbidva  3201  2ralbida  3261  spcimgft  3505  copsexgw  5446  copsexg  5447  pofun  5558  imainss  6120  fvmptdf  6956  eqfnfv2  6986  fnex  7173  f1elima  7219  fliftfun  7268  isores2  7289  f1oiso  7307  ovmpodxf  7518  sorpssuni  7687  sorpssint  7688  tfindsg2  7814  2ndconst  8053  poxp2  8095  sexp3  8105  poseq  8110  oalim  8469  omlim  8470  oaass  8498  omlimcl  8515  omass  8517  oelim2  8533  oeoa  8535  oeoelem  8536  nnaass  8560  omabs  8589  eroveu  8761  sbthlem4  9030  fimaxg  9199  fisupg  9200  fofinf1o  9244  fiming  9415  fiinfg  9416  ordtypelem7  9441  hartogs  9461  card2on  9471  unwdomg  9501  wemapwe  9618  frmin  9673  dfac5  10051  cfsmolem  10192  isf32lem2  10276  ttukeylem6  10436  ondomon  10485  alephreg  10505  ltexprlem6  10964  recexsrlem  11026  wloglei  11681  recextlem2  11780  fimaxre  12098  creur  12151  uz11  12788  xrmaxeq  13106  xrmineq  13107  xaddf  13151  xaddass  13176  xleadd1a  13180  xlt2add  13187  xmullem  13191  xmulgt0  13210  xmulasslem3  13213  xlemul1a  13215  xadddilem  13221  fzrevral  13540  seqcaopr2  13973  expnlbnd2  14169  faclbnd4lem4  14231  hashgt23el  14359  rtrclreclem3  14995  rtrclreclem4  14996  relexpindlem  14998  rtrclind  15000  shftlem  15003  01sqrex  15184  cau3lem  15290  limsupbnd2  15418  clim2  15439  clim2c  15440  clim0c  15442  rlimresb  15500  2clim  15507  climabs0  15520  climcn1  15527  climcn2  15528  o1rlimmul  15554  climsqz  15576  climsqz2  15577  rlimsqzlem  15584  lo1le  15587  climsup  15605  caucvgrlem2  15610  iseralt  15620  summolem2  15651  fsum2dlem  15705  cvgcmp  15751  cvgcmpce  15753  climfsum  15755  fsumiun  15756  geomulcvg  15811  mertenslem2  15820  mertens  15821  prodfn0  15829  prodfrec  15830  zprod  15872  fprodeq0  15910  fprodn0  15914  fprod2dlem  15915  smu01lem  16424  gcdcllem1  16438  dvdssq  16506  lcmdvds  16547  coprmdvds2  16593  pclem  16778  pcge0  16802  pcgcd1  16817  prmpwdvds  16844  1arithlem4  16866  4sqlem18  16902  vdwlem10  16930  vdwlem11  16931  ramval  16948  ramub1lem2  16967  ramcl  16969  imasaddfnlem  17461  imasaddflem  17463  imasvscafn  17470  imasleval  17474  ismon2  17670  isepi2  17677  issubc3  17785  cofucl  17824  setcmon  18023  setcepi  18024  ipodrsfi  18474  ipodrsima  18476  isacs3lem  18477  grpidpropd  18599  grprida  18612  gsumpropd2lem  18616  mgmhmpropd  18635  mgmhmima  18652  mhmpropd  18729  mhmimalem  18761  grplcan  18942  dfgrp3lem  18980  mulgdirlem  19047  subgmulg  19082  issubg4  19087  subgint  19092  ssnmz  19107  cycsubgcl  19147  gastacl  19250  orbsta  19254  cntzsubg  19280  galactghm  19345  odmulg  19497  odbezout  19499  sylow3lem2  19569  lsmsubm  19594  efgsfo  19680  mulgmhm  19768  mulgghm  19769  gsumval3  19848  gsumcllem  19849  gsumpt  19903  gsum2d  19913  gsum2d2  19915  prdsgsum  19922  subgdmdprd  19977  dprd2d2  19987  ablfac1eu  20016  rngpropd  20121  srglmhm  20168  srgrmhm  20169  ringpropd  20235  ringlghm  20259  pwsgprod  20277  dvdsrpropd  20364  rhmimasubrnglem  20510  cntzsdrg  20747  abvpropd  20780  islmodd  20829  lmodprop2d  20887  lsssubg  20920  lsspropd  20981  lmhmima  21011  lidlsubg  21190  phlpropd  21622  frlmsslsp  21763  lindfmm  21794  islindf4  21805  assapropd  21839  asclpropd  21865  psrass1lem  21900  mplcoe1  22004  mplcoe5  22007  mplind  22037  evlslem2  22046  evlsval  22053  coe1tmmul2  22230  mamuass  22358  mavmulass  22505  mdetuni0  22577  mdetmul  22579  cpmatacl  22672  cpmadugsumfi  22833  cpmadumatpolylem1  22837  cpmadumatpolylem2  22838  cpmadumatpoly  22839  cayhamlem4  22844  neips  23069  neindisj  23073  ordtrest2lem  23159  lmbrf  23216  lmss  23254  isreg2  23333  lmmo  23336  hauscmplem  23362  bwth  23366  2ndcomap  23414  1stcelcls  23417  restlly  23439  islly2  23440  cldllycmp  23451  comppfsc  23488  1stckgenlem  23509  txbas  23523  txbasval  23562  tx1cn  23565  ptpjopn  23568  ptcnp  23578  txnlly  23593  txlm  23604  xkococn  23616  fgabs  23835  fmfnfmlem4  23913  flimcf  23938  hauspwpwf1  23943  fclsbas  23977  fclscf  23981  flimfnfcls  23984  ghmcnp  24071  tsmsxp  24111  isxmet2d  24283  elmopn2  24401  mopni3  24450  blsscls2  24460  metequiv2  24466  metss2lem  24467  met2ndci  24478  metrest  24480  metcnp  24497  metcnp2  24498  metcnpi3  24502  txmetcnp  24503  nmolb2d  24674  xrge0tsms  24791  metdsre  24810  metnrmlem3  24818  fsumcn  24829  elcncf2  24851  mulc1cncf  24866  cncfco  24868  cncfmet  24870  bndth  24925  evth  24926  copco  24986  pcopt2  24991  pcoass  24992  pcorevlem  24994  lmmcvg  25229  lmmbrf  25230  iscau4  25247  iscauf  25248  cmetcaulem  25256  iscmet3lem3  25258  iscmet3lem1  25259  causs  25266  equivcfil  25267  lmclim  25271  caubl  25276  caublcls  25277  bcth3  25299  ivthle  25425  ivthle2  25426  ovoliunlem1  25471  ovolicc2lem5  25490  volsuplem  25524  uniioombllem6  25557  dyaddisjlem  25564  dyadmax  25567  volcn  25575  mbfmulc2lem  25616  ismbf3d  25623  mbfsup  25633  mbfinf  25634  mbflim  25637  i1fmullem  25663  itg2seq  25711  itg2uba  25712  itg2splitlem  25717  itg2split  25718  itg2monolem1  25719  bddiblnc  25811  ditgsplitlem  25829  ellimc2  25846  ellimc3  25848  limcflf  25850  limcmpt  25852  limcco  25862  lhop1lem  25986  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumrlim  26006  ftc1a  26012  ftc1lem6  26016  mdegmullem  26051  elply2  26169  plypf1  26185  ulmcaulem  26371  ulmcau  26372  ulmss  26374  ulmdvlem3  26379  mtest  26381  itgulm  26385  abelthlem8  26417  abelth  26419  tanord  26515  cxpcn3lem  26725  mcubic  26825  cubic2  26826  dvdsflsumcom  27166  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  lgsdchrval  27333  2sqlem9  27406  rplogsumlem2  27464  rpvmasumlem  27466  dchrvmasumlem1  27474  vmalogdivsum2  27517  logsqvma  27521  selberg  27527  selberg4  27540  pntibndlem3  27571  pntlem3  27588  pntleml  27590  padicabv  27609  padicabvf  27610  padicabvcxp  27611  ostth3  27617  nosupbnd1lem5  27692  noinfbnd1lem5  27707  nocvxminlem  27762  lrrecfr  27951  addsprop  27984  mulsproplem9  28132  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  mulsprop  28138  lemulsd  28146  mulsuniflem  28157  mulsasslem3  28173  axpasch  29026  axcontlem7  29055  axcontlem10  29058  cusgrsize2inds  29539  grpolcan  30617  nvmul0or  30737  nmosetre  30851  blocnilem  30891  blocni  30892  h2hcau  31066  h2hlm  31067  shsel3  31402  chscllem2  31725  homulcl  31846  adjsym  31920  cnvadj  31979  hhcno  31991  hhcnf  31992  lnopl  32001  unoplin  32007  counop  32008  lnfnl  32018  hmoplin  32029  hmopm  32108  nmcexi  32113  lnconi  32120  riesz3i  32149  leopmuli  32220  leopmul  32221  hstle  32317  mdsl0  32397  mdslmd1lem2  32413  atcvatlem  32472  chirredi  32481  cdj1i  32520  sbc2iedf  32550  foresf1o  32590  suppovss  32770  isoun  32791  difioo  32872  swrdf1  33048  xrge0tsmsd  33166  cycpmrn  33236  ressply1invg  33661  ply1unit  33667  fedgmullem2  33807  pstmxmet  34074  ordtrest2NEWlem  34099  esum2dlem  34269  esum2d  34270  dya2icoseg2  34455  eulerpartlemgc  34539  eulerpartlemgh  34555  eulerpartlemgs2  34557  ballotlemimin  34683  signstfvneq0  34749  hgt750lemb  34833  connpconn  35448  cvmliftmolem2  35495  cvmliftlem6  35503  cvmliftlem8  35505  cvmlift2lem12  35527  elmrsubrn  35733  dfon2lem6  35999  ifscgr  36257  brsegle  36321  neibastop2lem  36573  bj-elabd2ALT  37167  bj-ismooredr2  37357  curf  37843  finixpnum  37850  fin2solem  37851  fin2so  37852  lindsenlbs  37860  matunitlindflem1  37861  matunitlindflem2  37862  matunitlindf  37863  poimirlem3  37868  poimirlem4  37869  poimirlem6  37871  poimirlem7  37872  poimirlem14  37879  poimirlem16  37881  poimirlem19  37884  poimirlem22  37887  poimirlem28  37893  poimirlem29  37894  poimirlem30  37895  poimir  37898  heicant  37900  itg2gt0cn  37920  ftc1cnnc  37937  ftc1anclem5  37942  ftc1anclem6  37943  ftc1anclem7  37944  ftc1anc  37946  cover2  37960  filbcmb  37985  fdc  37990  fdc1  37991  seqpo  37992  incsequz  37993  incsequz2  37994  metf1o  38000  lmclim2  38003  geomcau  38004  isbnd2  38028  bndss  38031  ismtybndlem  38051  heibor1lem  38054  rrncmslem  38077  rrnequiv  38080  exidreslem  38122  ghomco  38136  isdrngo3  38204  rngoisocnv  38226  isidlc  38260  idlnegcl  38267  divrngidl  38273  intidl  38274  unichnidl  38276  keridl  38277  igenmin  38309  prnc  38312  ispridlc  38315  erimeq2  39008  prter3  39252  glbconxN  39748  atltcvr  39805  3dim1  39837  lvolnle3at  39952  linepsubN  40122  osumclN  40337  pexmidALTN  40348  lhpmatb  40401  cdlemg1idlemN  40942  dihlss  41620  dihglblem5aN  41662  dihatlat  41704  aks6d1c1p1  42471  aks6d1c5lem1  42500  unitscyglem4  42562  f1o2d2  42599  selvvvval  42937  fsuppind  42942  fsuppssindlem1  42943  prjspertr  42957  prjspreln0  42961  lsmfgcl  43425  kercvrlsm  43434  unxpwdom3  43446  hbt  43481  oa0suclim  43626  om0suclim  43627  oe0suclim  43628  naddcnff  43713  cvgdvgrat  44663  climinf  45960  clim2f  45988  clim2cf  46002  clim0cf  46006  clim2f2  46022  fmtnofac2lem  47922  ovmpordxf  48693  oppcthinendcALT  49794  cotsqcscsq  50115  aacllem  50154