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  3045  ralimdvva  3211  reximdvva  3212  2ralbidva  3226  2rexbidva  3227  2ralbida  3287  spcimgft  3513  copsexgwOLD  5471  copsexg  5472  pofun  5585  imainss  6149  fvmptdf  6997  eqfnfv2  7027  fnex  7220  f1elima  7264  fliftfun  7317  isores2  7338  f1oiso  7356  ovmpodxf  7567  sorpssuni  7737  sorpssint  7738  tfindsg2  7862  2ndconst  8102  mpof1o2d  8127  poxp2  8145  sexp3  8155  poseq  8160  oalim  8523  omlim  8524  oaass  8552  omlimcl  8569  omass  8571  oelim2  8587  oeoa  8589  oeoelem  8590  nnaass  8614  omabs  8643  eroveu  8816  curf  8873  sbthlem4  9092  fimaxg  9261  fisupg  9262  fofinf1o  9303  fiming  9474  fiinfg  9475  ordtypelem7  9500  hartogs  9520  card2on  9530  unwdomg  9560  wemapwe  9680  frmin  9735  dfac5  10135  cfsmolem  10276  isf32lem2  10360  ttukeylem6  10520  ondomon  10575  alephreg  10595  ltexprlem6  11054  recexsrlem  11116  wloglei  11774  recextlem2  11873  fimaxre  12187  creur  12240  uz11  12916  xrmaxeq  13235  xrmineq  13236  xaddf  13280  xaddass  13305  xleadd1a  13309  xlt2add  13316  xmullem  13320  xmulgt0  13339  xmulasslem3  13342  xlemul1a  13344  xadddilem  13350  fzrevral  13671  seqcaopr2  14106  expnlbnd2  14302  faclbnd4lem4  14364  hashgt23el  14493  swrdf1  14723  rtrclreclem3  15137  rtrclreclem4  15138  relexpindlem  15140  rtrclind  15142  shftlem  15145  01sqrex  15340  cau3lem  15446  limsupbnd2  15574  clim2  15595  clim2c  15596  clim0c  15598  rlimresb  15656  2clim  15663  climabs0  15676  climcn1  15683  climcn2  15684  o1rlimmul  15710  climsqz  15732  climsqz2  15733  rlimsqzlem  15740  lo1le  15743  climsup  15761  caucvgrlem2  15766  iseralt  15776  summolem2  15806  fsum2dlem  15860  cvgcmp  15907  cvgcmpce  15909  climfsum  15911  fsumiun  15912  geomulcvg  15969  mertenslem2  15978  mertens  15979  prodfn0  15987  prodfrec  15988  zprod  16030  fprodeq0  16068  fprodn0  16072  fprod2dlem  16073  smu01lem  16581  gcdcllem1  16595  dvdssq  16663  lcmdvds  16704  coprmdvds2  16750  pclem  16936  pcge0  16960  pcgcd1  16975  prmpwdvds  17002  1arithlem4  17024  4sqlem18  17060  vdwlem10  17088  vdwlem11  17089  ramval  17106  ramub1lem2  17125  ramcl  17127  imasaddfnlem  17620  imasaddflem  17622  imasvscafn  17629  imasleval  17633  ismon2  17829  isepi2  17836  issubc3  17944  cofucl  17983  setcmon  18182  setcepi  18183  ipodrsfi  18633  ipodrsima  18635  isacs3lem  18636  grpidpropd  18761  grprida  18775  gsumpropd2lem  18787  mgmhmpropd  18806  mgmhmima  18823  mhmpropd  18906  mhmimalem  18939  grplcan  19130  dfgrp3lem  19167  mulgdirlem  19234  subgmulg  19270  issubg4  19275  subgint  19280  ssnmz  19295  cycsubgcl  19340  gastacl  19442  orbsta  19446  cntzsubg  19472  galactghm  19537  odmulg  19689  odbezout  19691  sylow3lem2  19761  lsmsubm  19786  efgsfo  19872  mulgmhm  19960  mulgghm  19961  gsumval3  20040  gsumcllem  20041  gsumpt  20095  gsum2d  20105  gsum2d2  20107  prdsgsum  20114  subgdmdprd  20169  dprd2d2  20179  ablfac1eu  20208  rngpropd  20315  srglmhm  20366  srgrmhm  20367  ringpropd  20436  ringlghm  20460  pwsgprod  20476  dvdsrpropd  20563  rhmimasubrnglem  20733  isdrng5  20923  cntzsdrg  20974  abvpropd  21007  islmodd  21056  lmodprop2d  21114  lsssubg  21147  lsspropd  21207  lmhmima  21237  lidlsubg  21417  phlpropd  21874  frlmsslsp  22015  lindfmm  22046  islindf4  22057  lindsenlbs  22070  assapropd  22092  asclpropd  22118  psrass1lem  22154  mplcoe1  22259  mplcoe5  22262  mplind  22292  evlslem2  22301  evlsval  22308  selvvvval  22364  coe1tmmul2  22508  mamuass  22630  mavmulass  22777  mdetuni0  22849  mdetmul  22851  matunitlindflem1  22907  matunitlindflem2  22908  matunitlindf  22909  cpmatacl  22947  cpmadugsumfi  23108  cpmadumatpolylem1  23112  cpmadumatpolylem2  23113  cpmadumatpoly  23114  cayhamlem4  23119  neips  23344  neindisj  23348  ordtrest2lem  23434  lmbrf  23491  lmss  23529  isreg2  23608  lmmo  23611  hauscmplem  23637  bwth  23641  2ndcomap  23690  1stcelcls  23693  restlly  23715  islly2  23716  cldllycmp  23727  comppfsc  23764  1stckgenlem  23785  txbas  23799  txbasval  23838  tx1cn  23841  ptpjopn  23844  ptcnp  23854  txnlly  23869  txlm  23880  xkococn  23892  fgabs  24111  fmfnfmlem4  24189  flimcf  24214  hauspwpwf1  24219  fclsbas  24253  fclscf  24257  flimfnfcls  24260  ghmcnp  24347  tsmsxp  24387  isxmet2d  24559  elmopn2  24677  mopni3  24726  blsscls2  24736  metequiv2  24742  metss2lem  24743  met2ndci  24754  metrest  24756  metcnp  24773  metcnp2  24774  metcnpi3  24778  txmetcnp  24779  nmolb2d  24950  xrge0tsms  25067  metdsre  25086  metnrmlem3  25094  fsumcn  25104  elcncf2  25124  mulc1cncf  25139  cncfco  25141  cncfmet  25143  bndth  25192  evth  25193  copco  25252  pcopt2  25257  pcoass  25258  pcorevlem  25260  lmmcvg  25495  lmmbrf  25496  iscau4  25513  iscauf  25514  cmetcaulem  25522  iscmet3lem3  25524  iscmet3lem1  25525  causs  25532  equivcfil  25533  lmclim  25537  caubl  25542  caublcls  25543  bcth3  25565  ivthle  25690  ivthle2  25691  ovoliunlem1  25736  ovolicc2lem5  25755  volsuplem  25789  uniioombllem6  25822  dyaddisjlem  25829  dyadmax  25832  volcn  25840  mbfmulc2lem  25881  ismbf3d  25888  mbfsup  25898  mbfinf  25899  mbflim  25902  i1fmullem  25928  itg2seq  25976  itg2uba  25977  itg2splitlem  25982  itg2split  25983  itg2monolem1  25984  bddiblnc  26076  ditgsplitlem  26094  ellimc2  26111  ellimc3  26113  limcflf  26115  limcmpt  26117  limcco  26127  lhop1lem  26247  dvfsumle  26255  dvfsumabs  26257  dvfsumrlim  26265  ftc1a  26271  ftc1lem6  26275  mdegmullem  26310  elply2  26428  plypf1  26445  ulmcaulem  26637  ulmcau  26638  ulmss  26640  ulmdvlem3  26645  mtest  26647  itgulm  26651  abelthlem8  26682  abelth  26684  tanord  26783  cxpcn3lem  26992  mcubic  27092  cubic2  27093  dvdsflsumcom  27432  fsumdvdsmul  27439  lgsdchrval  27598  2sqlem9  27671  rplogsumlem2  27729  rpvmasumlem  27731  dchrvmasumlem1  27739  vmalogdivsum2  27782  logsqvma  27786  selberg  27792  selberg4  27805  pntibndlem3  27836  pntlem3  27853  pntleml  27855  padicabv  27874  padicabvf  27875  padicabvcxp  27876  ostth3  27882  nosupbnd1lem5  27956  noinfbnd1lem5  27971  nocvxminlem  28027  lrrecfr  28216  addsprop  28249  mulsproplem9  28397  mulsproplem12  28400  mulsproplem13  28401  mulsproplem14  28402  mulsprop  28403  lemulsd  28411  mulsuniflem  28422  mulsasslem3  28438  axpasch  29406  axcontlem7  29435  axcontlem10  29438  cusgrsize2inds  29921  grpolcan  31019  nvmul0or  31139  nmosetre  31253  blocnilem  31293  blocni  31294  h2hcau  31468  h2hlm  31469  shsel3  31804  chscllem2  32127  homulcl  32248  adjsym  32322  cnvadj  32381  hhcno  32393  hhcnf  32394  lnopl  32403  unoplin  32409  counop  32410  lnfnl  32420  hmoplin  32431  hmopm  32510  nmcexi  32515  lnconi  32522  riesz3i  32551  leopmuli  32622  leopmul  32623  hstle  32719  mdsl0  32799  mdslmd1lem2  32815  atcvatlem  32874  chirredi  32883  cdj1i  32922  sbc2iedf  32949  foresf1o  32987  suppovss  33161  isoun  33182  difioo  33261  xrge0tsmsd  33521  cycpmrn  33591  ressply1invg  33987  ply1unit  33993  fedgmullem2  34148  pstmxmet  34415  ordtrest2NEWlem  34440  esum2dlem  34610  esum2d  34611  dya2icoseg2  34797  eulerpartlemgc  34881  eulerpartlemgh  34897  eulerpartlemgs2  34899  ballotlemimin  35025  signstfvneq0  35088  hgt750lemb  35172  connpconn  35822  cvmliftmolem2  35869  cvmliftlem6  35877  cvmliftlem8  35879  cvmlift2lem12  35901  elmrsubrn  36107  dfon2lem6  36373  ifscgr  36632  brsegle  36696  neibastop2lem  36987  bj-elabd2ALT  37677  bj-ismooredr2  37868  finixpnum  38367  fin2solem  38368  fin2so  38369  poimirlem3  38380  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem14  38391  poimirlem16  38393  poimirlem19  38396  poimirlem22  38399  poimirlem28  38405  poimirlem29  38406  poimirlem30  38407  poimir  38410  heicant  38412  itg2gt0cn  38432  ftc1cnnc  38449  ftc1anclem5  38454  ftc1anclem6  38455  ftc1anclem7  38456  ftc1anc  38458  cover2  38473  filbcmb  38498  fdc  38503  fdc1  38504  seqpo  38505  incsequz  38506  incsequz2  38507  metf1o  38513  lmclim2  38516  geomcau  38517  isbnd2  38541  bndss  38544  ismtybndlem  38564  heibor1lem  38567  rrncmslem  38590  rrnequiv  38593  exidreslem  38635  ghomco  38649  isdrngo3  38717  rngoisocnv  38739  isidlc  38773  idlnegcl  38780  divrngidl  38786  intidl  38787  unichnidl  38789  keridl  38790  igenmin  38822  prnc  38825  ispridlc  38828  erimeq2  39519  prter3  39763  glbconxN  40259  atltcvr  40316  3dim1  40348  lvolnle3at  40463  linepsubN  40633  osumclN  40848  pexmidALTN  40859  lhpmatb  40912  cdlemg1idlemN  41453  dihlss  42131  dihglblem5aN  42173  dihatlat  42215  aks6d1c1p1  42981  aks6d1c5lem1  43010  unitscyglem4  43072  fsuppind  43444  fsuppssindlem1  43445  prjspertr  43459  prjspreln0  43463  lsmfgcl  43923  kercvrlsm  43932  unxpwdom3  43944  hbt  43979  oa0suclim  44124  om0suclim  44125  oe0suclim  44126  naddcnff  44211  cvgdvgrat  45145  climinf  46444  clim2f  46472  clim2cf  46486  clim0cf  46490  clim2f2  46506  fmtnofac2lem  48479  ovmpordxf  49277  oppcthinendcALT  50375  cotsqcscsq  50696  aacllem  50780