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  3049  ralimdvva  3215  reximdvva  3216  2ralbidva  3230  2rexbidva  3231  2ralbida  3291  spcimgft  3518  copsexgwOLD  5478  copsexg  5479  pofun  5592  imainss  6156  fvmptdf  7003  eqfnfv2  7033  fnex  7222  f1elima  7268  fliftfun  7321  isores2  7342  f1oiso  7360  ovmpodxf  7573  sorpssuni  7742  sorpssint  7743  tfindsg2  7867  2ndconst  8105  mpof1o2d  8130  poxp2  8148  sexp3  8158  poseq  8163  oalim  8526  omlim  8527  oaass  8555  omlimcl  8572  omass  8574  oelim2  8590  oeoa  8592  oeoelem  8593  nnaass  8617  omabs  8646  eroveu  8819  sbthlem4  9088  fimaxg  9257  fisupg  9258  fofinf1o  9299  fiming  9470  fiinfg  9471  ordtypelem7  9496  hartogs  9516  card2on  9526  unwdomg  9556  wemapwe  9676  frmin  9731  dfac5  10131  cfsmolem  10272  isf32lem2  10356  ttukeylem6  10516  ondomon  10565  alephreg  10585  ltexprlem6  11044  recexsrlem  11106  wloglei  11764  recextlem2  11863  fimaxre  12177  creur  12230  uz11  12905  xrmaxeq  13223  xrmineq  13224  xaddf  13268  xaddass  13293  xleadd1a  13297  xlt2add  13304  xmullem  13308  xmulgt0  13327  xmulasslem3  13330  xlemul1a  13332  xadddilem  13338  fzrevral  13659  seqcaopr2  14094  expnlbnd2  14290  faclbnd4lem4  14352  hashgt23el  14481  swrdf1  14711  rtrclreclem3  15123  rtrclreclem4  15124  relexpindlem  15126  rtrclind  15128  shftlem  15131  01sqrex  15326  cau3lem  15432  limsupbnd2  15560  clim2  15581  clim2c  15582  clim0c  15584  rlimresb  15642  2clim  15649  climabs0  15662  climcn1  15669  climcn2  15670  o1rlimmul  15696  climsqz  15718  climsqz2  15719  rlimsqzlem  15726  lo1le  15729  climsup  15747  caucvgrlem2  15752  iseralt  15762  summolem2  15793  fsum2dlem  15847  cvgcmp  15894  cvgcmpce  15896  climfsum  15898  fsumiun  15899  geomulcvg  15956  mertenslem2  15965  mertens  15966  prodfn0  15974  prodfrec  15975  zprod  16017  fprodeq0  16055  fprodn0  16059  fprod2dlem  16060  smu01lem  16568  gcdcllem1  16582  dvdssq  16650  lcmdvds  16691  coprmdvds2  16737  pclem  16923  pcge0  16947  pcgcd1  16962  prmpwdvds  16989  1arithlem4  17011  4sqlem18  17047  vdwlem10  17075  vdwlem11  17076  ramval  17093  ramub1lem2  17112  ramcl  17114  imasaddfnlem  17607  imasaddflem  17609  imasvscafn  17616  imasleval  17620  ismon2  17816  isepi2  17823  issubc3  17931  cofucl  17970  setcmon  18169  setcepi  18170  ipodrsfi  18620  ipodrsima  18622  isacs3lem  18623  grpidpropd  18745  grprida  18759  gsumpropd2lem  18766  mgmhmpropd  18785  mgmhmima  18802  mhmpropd  18881  mhmimalem  18914  grplcan  19098  dfgrp3lem  19135  mulgdirlem  19202  subgmulg  19238  issubg4  19243  subgint  19248  ssnmz  19263  cycsubgcl  19308  gastacl  19410  orbsta  19414  cntzsubg  19440  galactghm  19505  odmulg  19657  odbezout  19659  sylow3lem2  19729  lsmsubm  19754  efgsfo  19840  mulgmhm  19928  mulgghm  19929  gsumval3  20008  gsumcllem  20009  gsumpt  20063  gsum2d  20073  gsum2d2  20075  prdsgsum  20082  subgdmdprd  20137  dprd2d2  20147  ablfac1eu  20176  rngpropd  20283  srglmhm  20334  srgrmhm  20335  ringpropd  20404  ringlghm  20428  pwsgprod  20444  dvdsrpropd  20531  rhmimasubrnglem  20701  isdrng5  20891  cntzsdrg  20942  abvpropd  20975  islmodd  21024  lmodprop2d  21082  lsssubg  21115  lsspropd  21175  lmhmima  21205  lidlsubg  21385  phlpropd  21842  frlmsslsp  21983  lindfmm  22014  islindf4  22025  assapropd  22058  asclpropd  22084  psrass1lem  22120  mplcoe1  22225  mplcoe5  22228  mplind  22258  evlslem2  22267  evlsval  22274  selvvvval  22330  coe1tmmul2  22474  mamuass  22596  mavmulass  22743  mdetuni0  22815  mdetmul  22817  cpmatacl  22910  cpmadugsumfi  23071  cpmadumatpolylem1  23075  cpmadumatpolylem2  23076  cpmadumatpoly  23077  cayhamlem4  23082  neips  23307  neindisj  23311  ordtrest2lem  23397  lmbrf  23454  lmss  23492  isreg2  23571  lmmo  23574  hauscmplem  23600  bwth  23604  2ndcomap  23652  1stcelcls  23655  restlly  23677  islly2  23678  cldllycmp  23689  comppfsc  23726  1stckgenlem  23747  txbas  23761  txbasval  23800  tx1cn  23803  ptpjopn  23806  ptcnp  23816  txnlly  23831  txlm  23842  xkococn  23854  fgabs  24073  fmfnfmlem4  24151  flimcf  24176  hauspwpwf1  24181  fclsbas  24215  fclscf  24219  flimfnfcls  24222  ghmcnp  24309  tsmsxp  24349  isxmet2d  24521  elmopn2  24639  mopni3  24688  blsscls2  24698  metequiv2  24704  metss2lem  24705  met2ndci  24716  metrest  24718  metcnp  24735  metcnp2  24736  metcnpi3  24740  txmetcnp  24741  nmolb2d  24912  xrge0tsms  25029  metdsre  25048  metnrmlem3  25056  fsumcn  25066  elcncf2  25086  mulc1cncf  25101  cncfco  25103  cncfmet  25105  bndth  25154  evth  25155  copco  25214  pcopt2  25219  pcoass  25220  pcorevlem  25222  lmmcvg  25457  lmmbrf  25458  iscau4  25475  iscauf  25476  cmetcaulem  25484  iscmet3lem3  25486  iscmet3lem1  25487  causs  25494  equivcfil  25495  lmclim  25499  caubl  25504  caublcls  25505  bcth3  25527  ivthle  25652  ivthle2  25653  ovoliunlem1  25698  ovolicc2lem5  25717  volsuplem  25751  uniioombllem6  25784  dyaddisjlem  25791  dyadmax  25794  volcn  25802  mbfmulc2lem  25843  ismbf3d  25850  mbfsup  25860  mbfinf  25861  mbflim  25864  i1fmullem  25890  itg2seq  25938  itg2uba  25939  itg2splitlem  25944  itg2split  25945  itg2monolem1  25946  bddiblnc  26038  ditgsplitlem  26056  ellimc2  26073  ellimc3  26075  limcflf  26077  limcmpt  26079  limcco  26089  lhop1lem  26209  dvfsumle  26217  dvfsumabs  26219  dvfsumrlim  26227  ftc1a  26233  ftc1lem6  26237  mdegmullem  26272  elply2  26390  plypf1  26406  ulmcaulem  26594  ulmcau  26595  ulmss  26597  ulmdvlem3  26602  mtest  26604  itgulm  26608  abelthlem8  26639  abelth  26641  tanord  26740  cxpcn3lem  26949  mcubic  27049  cubic2  27050  dvdsflsumcom  27389  fsumdvdsmul  27396  lgsdchrval  27555  2sqlem9  27628  rplogsumlem2  27686  rpvmasumlem  27688  dchrvmasumlem1  27696  vmalogdivsum2  27739  logsqvma  27743  selberg  27749  selberg4  27762  pntibndlem3  27793  pntlem3  27810  pntleml  27812  padicabv  27831  padicabvf  27832  padicabvcxp  27833  ostth3  27839  nosupbnd1lem5  27913  noinfbnd1lem5  27928  nocvxminlem  27984  lrrecfr  28173  addsprop  28206  mulsproplem9  28354  mulsproplem12  28357  mulsproplem13  28358  mulsproplem14  28359  mulsprop  28360  lemulsd  28368  mulsuniflem  28379  mulsasslem3  28395  axpasch  29328  axcontlem7  29357  axcontlem10  29360  cusgrsize2inds  29840  grpolcan  30919  nvmul0or  31039  nmosetre  31153  blocnilem  31193  blocni  31194  h2hcau  31368  h2hlm  31369  shsel3  31704  chscllem2  32027  homulcl  32148  adjsym  32222  cnvadj  32281  hhcno  32293  hhcnf  32294  lnopl  32303  unoplin  32309  counop  32310  lnfnl  32320  hmoplin  32331  hmopm  32410  nmcexi  32415  lnconi  32422  riesz3i  32451  leopmuli  32522  leopmul  32523  hstle  32619  mdsl0  32699  mdslmd1lem2  32715  atcvatlem  32774  chirredi  32783  cdj1i  32822  sbc2iedf  32849  foresf1o  32887  suppovss  33063  isoun  33084  difioo  33164  xrge0tsmsd  33424  cycpmrn  33494  ressply1invg  33890  ply1unit  33896  fedgmullem2  34051  pstmxmet  34318  ordtrest2NEWlem  34343  esum2dlem  34513  esum2d  34514  dya2icoseg2  34700  eulerpartlemgc  34784  eulerpartlemgh  34800  eulerpartlemgs2  34802  ballotlemimin  34928  signstfvneq0  34991  hgt750lemb  35075  connpconn  35748  cvmliftmolem2  35795  cvmliftlem6  35803  cvmliftlem8  35805  cvmlift2lem12  35827  elmrsubrn  36033  dfon2lem6  36299  ifscgr  36557  brsegle  36621  neibastop2lem  36912  bj-elabd2ALT  37602  bj-ismooredr2  37793  curf  38290  finixpnum  38297  fin2solem  38298  fin2so  38299  lindsenlbs  38307  matunitlindflem1  38308  matunitlindflem2  38309  matunitlindf  38310  poimirlem3  38315  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem14  38326  poimirlem16  38328  poimirlem19  38331  poimirlem22  38334  poimirlem28  38340  poimirlem29  38341  poimirlem30  38342  poimir  38345  heicant  38347  itg2gt0cn  38367  ftc1cnnc  38384  ftc1anclem5  38389  ftc1anclem6  38390  ftc1anclem7  38391  ftc1anc  38393  cover2  38407  filbcmb  38432  fdc  38437  fdc1  38438  seqpo  38439  incsequz  38440  incsequz2  38441  metf1o  38447  lmclim2  38450  geomcau  38451  isbnd2  38475  bndss  38478  ismtybndlem  38498  heibor1lem  38501  rrncmslem  38524  rrnequiv  38527  exidreslem  38569  ghomco  38583  isdrngo3  38651  rngoisocnv  38673  isidlc  38707  idlnegcl  38714  divrngidl  38720  intidl  38721  unichnidl  38723  keridl  38724  igenmin  38756  prnc  38759  ispridlc  38762  erimeq2  39453  prter3  39697  glbconxN  40193  atltcvr  40250  3dim1  40282  lvolnle3at  40397  linepsubN  40567  osumclN  40782  pexmidALTN  40793  lhpmatb  40846  cdlemg1idlemN  41387  dihlss  42065  dihglblem5aN  42107  dihatlat  42149  aks6d1c1p1  42915  aks6d1c5lem1  42944  unitscyglem4  43006  fsuppind  43363  fsuppssindlem1  43364  prjspertr  43378  prjspreln0  43382  lsmfgcl  43842  kercvrlsm  43851  unxpwdom3  43863  hbt  43898  oa0suclim  44043  om0suclim  44044  oe0suclim  44045  naddcnff  44130  cvgdvgrat  45064  climinf  46363  clim2f  46391  clim2cf  46405  clim0cf  46409  clim2f2  46425  fmtnofac2lem  48361  ovmpordxf  49160  oppcthinendcALT  50260  cotsqcscsq  50581  aacllem  50662