Theorem anassrs 470

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anass  471  anass1rs  653  anabss5  666  anabss7  671  mpanr1  701  pm2.61ddan  812  pm2.61dda  813  pm2.61da2ne  3105  ralimdvva  3179  2ralbidva  3198  2ralbida  3232  reximdvva  3277  2rexbidva  3299  copsexgw  5373  copsexg  5374  pofun  5485  imainss  6005  fvmptdf  6768  eqfnfv2  6797  fnex  6974  f1elima  7015  fliftfun  7059  isores2  7080  f1oiso  7098  ovmpodxf  7294  sorpssuni  7452  sorpssint  7453  tfindsg2  7570  2ndconst  7790  oalim  8151  omlim  8152  oaass  8181  omlimcl  8198  omass  8200  oelim2  8215  oeoa  8217  oeoelem  8218  nnaass  8242  omabs  8268  eroveu  8386  sbthlem4  8624  fimaxg  8759  fisupg  8760  fofinf1o  8793  fiming  8956  fiinfg  8957  ordtypelem7  8982  hartogs  9002  card2on  9012  unwdomg  9042  wemapwe  9154  dfac5  9548  cfsmolem  9686  isf32lem2  9770  ttukeylem6  9930  ondomon  9979  alephreg  9998  ltexprlem6  10457  recexsrlem  10519  wloglei  11166  recextlem2  11265  fimaxre  11578  fimaxreOLD  11579  creur  11626  uz11  12261  xrmaxeq  12566  xrmineq  12567  xaddf  12611  xaddass  12636  xleadd1a  12640  xlt2add  12647  xmullem  12651  xmulgt0  12670  xmulasslem3  12673  xlemul1a  12675  xadddilem  12681  fzrevral  12986  seqcaopr2  13400  expnlbnd2  13589  faclbnd4lem4  13650  hashgt23el  13779  rtrclreclem3  14413  rtrclreclem4  14414  relexpindlem  14416  rtrclind  14418  shftlem  14421  01sqrex  14603  cau3lem  14708  limsupbnd2  14834  clim2  14855  clim2c  14856  clim0c  14858  rlimresb  14916  2clim  14923  climabs0  14936  climcn1  14942  climcn2  14943  o1rlimmul  14969  climsqz  14991  climsqz2  14992  rlimsqzlem  14999  lo1le  15002  climsup  15020  caucvgrlem2  15025  iseralt  15035  summolem2  15067  fsum2dlem  15119  cvgcmp  15165  cvgcmpce  15167  climfsum  15169  fsumiun  15170  geomulcvg  15226  mertenslem2  15235  mertens  15236  prodfn0  15244  prodfrec  15245  zprod  15285  fprodeq0  15323  fprodn0  15327  fprod2dlem  15328  smu01lem  15828  gcdcllem1  15842  gcdmultiplezOLD  15895  dvdssq  15905  lcmdvds  15946  coprmdvds2  15992  pclem  16169  pcge0  16192  pcgcd1  16207  prmpwdvds  16234  1arithlem4  16256  4sqlem18  16292  vdwlem10  16320  vdwlem11  16321  ramval  16338  ramub1lem2  16357  ramcl  16359  imasaddfnlem  16795  imasaddflem  16797  imasvscafn  16804  imasleval  16808  ismon2  16998  isepi2  17005  issubc3  17113  cofucl  17152  setcmon  17341  setcepi  17342  ipodrsfi  17767  ipodrsima  17769  isacs3lem  17770  grpidpropd  17866  grpridd  17879  gsumpropd2lem  17883  mhmpropd  17956  mhmima  17983  gsumccatOLD  17999  grplcan  18155  dfgrp3lem  18191  mulgdirlem  18252  subgmulg  18287  issubg4  18292  subgint  18297  ssnmz  18312  cycsubgcl  18343  gastacl  18433  orbsta  18437  cntzsubg  18461  galactghm  18526  odmulg  18677  odbezout  18679  sylow3lem2  18747  lsmsubm  18772  efgsfo  18859  mulgmhm  18942  mulgghm  18943  gsumval3  19021  gsumcllem  19022  gsumpt  19076  gsum2d  19086  gsum2d2  19088  prdsgsum  19095  subgdmdprd  19150  dprd2d2  19160  ablfac1eu  19189  srglmhm  19279  srgrmhm  19280  ringpropd  19326  ringlghm  19348  dvdsrpropd  19440  cntzsdrg  19575  abvpropd  19607  islmodd  19634  lmodprop2d  19690  lsssubg  19723  lsspropd  19783  lmhmima  19813  lidlsubg  19982  assapropd  20095  asclpropd  20120  psrass1lem  20151  mplcoe1  20240  mplcoe5  20243  mplind  20276  evlslem2  20286  evlsval  20293  coe1tmmul2  20438  phlpropd  20793  frlmsslsp  20934  lindfmm  20965  islindf4  20976  mamuass  21005  mavmulass  21152  mdetuni0  21224  mdetmul  21226  cpmatacl  21318  cpmadugsumfi  21479  cpmadumatpolylem1  21483  cpmadumatpolylem2  21484  cpmadumatpoly  21485  cayhamlem4  21490  neips  21715  neindisj  21719  ordtrest2lem  21805  lmbrf  21862  lmss  21900  isreg2  21979  lmmo  21982  hauscmplem  22008  bwth  22012  2ndcomap  22060  1stcelcls  22063  restlly  22085  islly2  22086  cldllycmp  22097  comppfsc  22134  1stckgenlem  22155  txbas  22169  txbasval  22208  tx1cn  22211  ptpjopn  22214  ptcnp  22224  txnlly  22239  txlm  22250  xkococn  22262  fgabs  22481  fmfnfmlem4  22559  flimcf  22584  hauspwpwf1  22589  fclsbas  22623  fclscf  22627  flimfnfcls  22630  ghmcnp  22717  tsmsxp  22757  isxmet2d  22931  elmopn2  23049  mopni3  23098  blsscls2  23108  metequiv2  23114  metss2lem  23115  met2ndci  23126  metrest  23128  metcnp  23145  metcnp2  23146  metcnpi3  23150  txmetcnp  23151  nmolb2d  23321  xrge0tsms  23436  metdsre  23455  metnrmlem3  23463  fsumcn  23472  elcncf2  23492  mulc1cncf  23507  cncfco  23509  cncfmet  23510  bndth  23556  evth  23557  copco  23616  pcopt2  23621  pcoass  23622  pcorevlem  23624  lmmcvg  23858  lmmbrf  23859  iscau4  23876  iscauf  23877  cmetcaulem  23885  iscmet3lem3  23887  iscmet3lem1  23888  causs  23895  equivcfil  23896  lmclim  23900  caubl  23905  caublcls  23906  bcth3  23928  ivthle  24051  ivthle2  24052  ovoliunlem1  24097  ovolicc2lem5  24116  volsuplem  24150  uniioombllem6  24183  dyaddisjlem  24190  dyadmax  24193  volcn  24201  mbfmulc2lem  24242  ismbf3d  24249  mbfsup  24259  mbfinf  24260  mbflim  24263  i1fmullem  24289  itg2seq  24337  itg2uba  24338  itg2splitlem  24343  itg2split  24344  itg2monolem1  24345  ditgsplitlem  24452  ellimc2  24469  ellimc3  24471  limcflf  24473  limcmpt  24475  limcco  24485  lhop1lem  24604  dvfsumle  24612  dvfsumabs  24614  dvfsumrlim  24622  ftc1a  24628  ftc1lem6  24632  mdegmullem  24666  elply2  24780  plypf1  24796  ulmcaulem  24976  ulmcau  24977  ulmss  24979  ulmdvlem3  24984  mtest  24986  itgulm  24990  abelthlem8  25021  abelth  25023  tanord  25116  cxpcn3lem  25322  mcubic  25419  cubic2  25420  dvdsflsumcom  25759  fsumdvdsmul  25766  lgsdchrval  25924  2sqlem9  25997  rplogsumlem2  26055  rpvmasumlem  26057  dchrvmasumlem1  26065  vmalogdivsum2  26108  logsqvma  26112  selberg  26118  selberg4  26131  pntibndlem3  26162  pntlem3  26179  pntleml  26181  padicabv  26200  padicabvf  26201  padicabvcxp  26202  ostth3  26208  axpasch  26721  axcontlem7  26750  axcontlem10  26753  cusgrsize2inds  27229  grpolcan  28301  nvmul0or  28421  nmosetre  28535  blocnilem  28575  blocni  28576  h2hcau  28750  h2hlm  28751  shsel3  29086  chscllem2  29409  homulcl  29530  adjsym  29604  cnvadj  29663  hhcno  29675  hhcnf  29676  lnopl  29685  unoplin  29691  counop  29692  lnfnl  29702  hmoplin  29713  hmopm  29792  nmcexi  29797  lnconi  29804  riesz3i  29833  leopmuli  29904  leopmul  29905  hstle  30001  mdsl0  30081  mdslmd1lem2  30097  atcvatlem  30156  chirredi  30165  cdj1i  30204  sbc2iedf  30224  foresf1o  30259  suppovss  30420  isoun  30431  difioo  30499  swrdf1  30625  xrge0tsmsd  30687  cycpmrn  30780  fedgmullem2  31021  pstmxmet  31132  ordtrest2NEWlem  31160  esum2dlem  31346  esum2d  31347  dya2icoseg2  31531  eulerpartlemgc  31615  eulerpartlemgh  31631  eulerpartlemgs2  31633  ballotlemimin  31758  signstfvneq0  31837  hgt750lemb  31922  connpconn  32477  cvmliftmolem2  32524  cvmliftlem6  32532  cvmliftlem8  32534  cvmlift2lem12  32556  elmrsubrn  32762  dfon2lem6  33028  poseq  33090  nosupbnd1lem5  33207  nocvxminlem  33242  ifscgr  33500  brsegle  33564  neibastop2lem  33703  bj-ismooredr2  34396  curf  34864  finixpnum  34871  fin2solem  34872  fin2so  34873  lindsenlbs  34881  matunitlindflem1  34882  matunitlindflem2  34883  matunitlindf  34884  poimirlem3  34889  poimirlem4  34890  poimirlem6  34892  poimirlem7  34893  poimirlem14  34900  poimirlem16  34902  poimirlem19  34905  poimirlem22  34908  poimirlem28  34914  poimirlem29  34915  poimirlem30  34916  poimir  34919  heicant  34921  itg2gt0cn  34941  bddiblnc  34956  ftc1cnnc  34960  ftc1anclem5  34965  ftc1anclem6  34966  ftc1anclem7  34967  ftc1anc  34969  cover2  34983  filbcmb  35009  fdc  35014  fdc1  35015  seqpo  35016  incsequz  35017  incsequz2  35018  metf1o  35024  lmclim2  35027  geomcau  35028  isbnd2  35055  bndss  35058  ismtybndlem  35078  heibor1lem  35081  rrncmslem  35104  rrnequiv  35107  exidreslem  35149  ghomco  35163  isdrngo3  35231  rngoisocnv  35253  isidlc  35287  idlnegcl  35294  divrngidl  35300  intidl  35301  unichnidl  35303  keridl  35304  igenmin  35336  prnc  35339  ispridlc  35342  erim2  35905  prter3  36012  glbconxN  36508  atltcvr  36565  3dim1  36597  lvolnle3at  36712  linepsubN  36882  osumclN  37097  pexmidALTN  37108  lhpmatb  37161  cdlemg1idlemN  37702  dihlss  38380  dihglblem5aN  38422  dihatlat  38464  prjspertr  39248  prjspreln0  39252  lsmfgcl  39667  kercvrlsm  39676  unxpwdom3  39688  hbt  39723  cvgdvgrat  40638  climinf  41880  clim2f  41910  clim2cf  41924  clim0cf  41928  clim2f2  41944  fmtnofac2lem  43724  isomuspgrlem2d  43990  mgmhmpropd  44046  mgmhmima  44063  ovmpordxf  44381  cotsqcscsq  44855  aacllem  44896