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  3043  ralimdvva  3209  reximdvva  3210  2ralbidva  3224  2rexbidva  3225  2ralbida  3285  spcimgft  3510  copsexgwOLD  5460  copsexg  5461  pofun  5576  imainss  6143  fvmptdf  7000  eqfnfv2  7030  fnex  7223  f1elima  7267  fliftfun  7320  isores2  7341  f1oiso  7359  ovmpodxf  7570  sorpssuni  7748  sorpssint  7749  tfindsg2  7873  2ndconst  8114  mpof1o2d  8139  poxp2  8162  sexp3  8172  poseq  8177  oalim  8543  omlim  8544  oaass  8572  omlimcl  8589  omass  8591  oelim2  8607  oeoa  8609  oeoelem  8610  nnaass  8634  omabs  8663  eroveu  8836  curf  8893  sbthlem4  9112  fimaxg  9281  fisupg  9282  fofinf1o  9324  fiming  9495  fiinfg  9496  ordtypelem7  9521  hartogs  9541  card2on  9551  unwdomg  9581  wemapwe  9701  frmin  9756  dfac5  10210  cfsmolem  10351  isf32lem2  10435  ttukeylem6  10595  ondomon  10650  alephreg  10670  ltexprlem6  11129  recexsrlem  11191  wloglei  11851  recextlem2  11950  fimaxre  12264  creur  12317  uz11  12993  xrmaxeq  13312  xrmineq  13313  xaddf  13357  xaddass  13382  xleadd1a  13386  xlt2add  13393  xmullem  13397  xmulgt0  13416  xmulasslem3  13419  xlemul1a  13421  xadddilem  13427  fzrevral  13749  seqcaopr2  14184  expnlbnd2  14381  faclbnd4lem4  14443  hashgt23el  14572  swrdf1  14803  rtrclreclem3  15218  rtrclreclem4  15219  relexpindlem  15221  rtrclind  15223  shftlem  15226  01sqrex  15421  cau3lem  15527  limsupbnd2  15655  clim2  15676  clim2c  15677  clim0c  15679  rlimresb  15737  2clim  15744  climabs0  15757  climcn1  15764  climcn2  15765  o1rlimmul  15791  climsqz  15813  climsqz2  15814  rlimsqzlem  15821  lo1le  15824  climsup  15842  caucvgrlem2  15847  iseralt  15857  summolem2  15887  fsum2dlem  15941  cvgcmp  15988  cvgcmpce  15990  climfsum  15992  fsumiun  15993  geomulcvg  16050  mertenslem2  16059  mertens  16060  prodfn0  16068  prodfrec  16069  zprod  16109  fprodeq0  16147  fprodn0  16151  fprod2dlem  16152  smu01lem  16660  gcdcllem1  16674  dvdssq  16747  lcmdvds  16788  coprmdvds2  16834  pclem  17021  pcge0  17045  pcgcd1  17060  prmpwdvds  17087  1arithlem4  17109  4sqlem18  17145  vdwlem10  17173  vdwlem11  17174  ramval  17191  ramub1lem2  17210  ramcl  17212  imasaddfnlem  17705  imasaddflem  17707  imasvscafn  17714  imasleval  17718  ismon2  17914  isepi2  17921  issubc3  18029  cofucl  18068  setcmon  18267  setcepi  18268  ipodrsfi  18718  ipodrsima  18720  isacs3lem  18721  grpidpropd  18847  grprida  18861  gsumpropd2lem  18873  mgmhmpropd  18892  mgmhmima  18909  mhmpropd  18992  mhmimalem  19025  grplcan  19216  dfgrp3lem  19253  mulgdirlem  19320  subgmulg  19356  issubg4  19361  subgint  19366  ssnmz  19381  cycsubgcl  19426  gastacl  19528  orbsta  19532  cntzsubg  19558  galactghm  19623  odmulg  19775  odbezout  19777  sylow3lem2  19847  lsmsubm  19872  efgsfo  19958  mulgmhm  20046  mulgghm  20047  gsumval3  20126  gsumcllem  20127  gsumpt  20181  gsum2d  20191  gsum2d2  20193  prdsgsum  20200  subgdmdprd  20255  dprd2d2  20265  ablfac1eu  20294  rngpropd  20401  srglmhm  20452  srgrmhm  20453  ringpropd  20524  ringlghm  20548  pwsgprod  20564  dvdsrpropd  20651  rhmimasubrnglem  20822  isdrng5  21013  cntzsdrg  21064  abvpropd  21097  islmodd  21146  lmodprop2d  21204  lsssubg  21237  lsspropd  21297  lmhmima  21327  lidlsubg  21507  phlpropd  21966  frlmsslsp  22107  lindfmm  22138  islindf4  22149  lindsenlbs  22162  assapropd  22184  asclpropd  22210  psrass1lem  22246  mplcoe1  22351  mplcoe5  22354  mplind  22384  evlslem2  22393  evlsval  22400  selvvvval  22456  coe1tmmul2  22600  mamuass  22722  mavmulass  22869  mdetuni0  22941  mdetmul  22943  matunitlindflem1  22999  matunitlindflem2  23000  matunitlindf  23001  cpmatacl  23039  cpmadugsumfi  23200  cpmadumatpolylem1  23204  cpmadumatpolylem2  23205  cpmadumatpoly  23206  cayhamlem4  23211  neips  23436  neindisj  23440  ordtrest2lem  23526  lmbrf  23583  lmss  23621  isreg2  23700  lmmo  23703  hauscmplem  23729  bwth  23733  2ndcomap  23782  1stcelcls  23785  restlly  23807  islly2  23808  cldllycmp  23819  comppfsc  23856  1stckgenlem  23877  txbas  23891  txbasval  23930  tx1cn  23933  ptpjopn  23936  ptcnp  23946  txnlly  23961  txlm  23972  xkococn  23984  fgabs  24203  fmfnfmlem4  24281  flimcf  24306  hauspwpwf1  24311  fclsbas  24345  fclscf  24349  flimfnfcls  24352  ghmcnp  24439  tsmsxp  24479  isxmet2d  24651  elmopn2  24769  mopni3  24818  blsscls2  24828  metequiv2  24834  metss2lem  24835  met2ndci  24846  metrest  24848  metcnp  24865  metcnp2  24866  metcnpi3  24870  txmetcnp  24871  nmolb2d  25042  xrge0tsms  25159  metdsre  25178  metnrmlem3  25186  fsumcn  25196  elcncf2  25216  mulc1cncf  25231  cncfco  25233  cncfmet  25235  bndth  25284  evth  25285  copco  25344  pcopt2  25349  pcoass  25350  pcorevlem  25352  lmmcvg  25587  lmmbrf  25588  iscau4  25605  iscauf  25606  cmetcaulem  25614  iscmet3lem3  25616  iscmet3lem1  25617  causs  25624  equivcfil  25625  lmclim  25629  caubl  25634  caublcls  25635  bcth3  25657  ivthle  25782  ivthle2  25783  ovoliunlem1  25828  ovolicc2lem5  25847  volsuplem  25881  uniioombllem6  25914  dyaddisjlem  25921  dyadmax  25924  volcn  25932  mbfmulc2lem  25973  ismbf3d  25980  mbfsup  25990  mbfinf  25991  mbflim  25994  i1fmullem  26020  itg2seq  26068  itg2uba  26069  itg2splitlem  26074  itg2split  26075  itg2monolem1  26076  bddiblnc  26167  ditgsplitlem  26185  ellimc2  26202  ellimc3  26204  limcflf  26206  limcmpt  26208  limcco  26218  lhop1lem  26338  dvfsumle  26346  dvfsumabs  26348  dvfsumrlim  26356  ftc1a  26362  ftc1lem6  26366  mdegmullem  26401  elply2  26519  plypf1  26536  ulmcaulem  26726  ulmcau  26727  ulmss  26729  ulmdvlem3  26734  mtest  26736  itgulm  26740  abelthlem8  26771  abelth  26773  tanord  26871  cxpcn3lem  27080  mcubic  27180  cubic2  27181  dvdsflsumcom  27520  fsumdvdsmul  27527  lgsdchrval  27686  2sqlem9  27759  rplogsumlem2  27817  rpvmasumlem  27819  dchrvmasumlem1  27827  vmalogdivsum2  27870  logsqvma  27874  selberg  27880  selberg4  27893  pntibndlem3  27924  pntlem3  27941  pntleml  27943  padicabv  27962  padicabvf  27963  padicabvcxp  27964  ostth3  27970  nosupbnd1lem5  28074  noinfbnd1lem5  28089  nocvxminlem  28145  lrrecfr  28334  addsprop  28367  mulsproplem9  28515  mulsproplem12  28518  mulsproplem13  28519  mulsproplem14  28520  mulsprop  28521  lemulsd  28529  mulsuniflem  28540  mulsasslem3  28556  axpasch  29524  axcontlem7  29553  axcontlem10  29556  cusgrsize2inds  30039  grpolcan  31137  nvmul0or  31257  nmosetre  31371  blocnilem  31411  blocni  31412  h2hcau  31586  h2hlm  31587  shsel3  31922  chscllem2  32245  homulcl  32366  adjsym  32440  cnvadj  32499  hhcno  32511  hhcnf  32512  lnopl  32521  unoplin  32527  counop  32528  lnfnl  32538  hmoplin  32549  hmopm  32628  nmcexi  32633  lnconi  32640  riesz3i  32669  leopmuli  32740  leopmul  32741  hstle  32837  mdsl0  32917  mdslmd1lem2  32933  atcvatlem  32992  chirredi  33001  cdj1i  33040  sbc2iedf  33109  foresf1o  33147  suppovss  33321  isoun  33342  difioo  33420  xrge0tsmsd  33680  cycpmrn  33750  ressply1invg  34147  ply1unit  34153  fedgmullem2  34308  pstmxmet  34575  ordtrest2NEWlem  34600  esum2dlem  34770  esum2d  34771  dya2icoseg2  34956  eulerpartlemgc  35040  eulerpartlemgh  35056  eulerpartlemgs2  35058  ballotlemimin  35184  signstfvneq0  35247  hgt750lemb  35331  connpconn  36086  cvmliftmolem2  36133  cvmliftlem6  36141  cvmliftlem8  36143  cvmlift2lem12  36165  elmrsubrn  36371  dfon2lem6  36642  ifscgr  36901  brsegle  36965  neibastop2lem  37240  bj-elabd2ALT  37930  bj-ismooredr2  38123  finixpnum  38621  fin2solem  38622  fin2so  38623  poimirlem3  38634  poimirlem4  38635  poimirlem6  38637  poimirlem7  38638  poimirlem14  38645  poimirlem16  38647  poimirlem19  38650  poimirlem22  38653  poimirlem28  38659  poimirlem29  38660  poimirlem30  38661  poimir  38664  heicant  38666  itg2gt0cn  38686  ftc1cnnc  38703  ftc1anclem5  38708  ftc1anclem6  38709  ftc1anclem7  38710  ftc1anc  38712  cover2  38742  filbcmb  38767  fdc  38772  fdc1  38773  seqpo  38774  incsequz  38775  incsequz2  38776  metf1o  38782  lmclim2  38785  geomcau  38786  isbnd2  38810  bndss  38813  ismtybndlem  38833  heibor1lem  38836  rrncmslem  38859  rrnequiv  38862  exidreslem  38904  ghomco  38918  isdrngo3  38986  rngoisocnv  39008  isidlc  39042  idlnegcl  39049  divrngidl  39055  intidl  39056  unichnidl  39058  keridl  39059  igenmin  39091  prnc  39094  ispridlc  39097  erimeq2  39788  prter3  40032  glbconxN  40528  atltcvr  40585  3dim1  40617  lvolnle3at  40732  linepsubN  40902  osumclN  41117  pexmidALTN  41128  lhpmatb  41181  cdlemg1idlemN  41722  dihlss  42400  dihglblem5aN  42442  dihatlat  42484  aks6d1c1p1  43250  aks6d1c5lem1  43279  unitscyglem4  43341  fsuppind  43711  fsuppssindlem1  43712  prjspertr  43726  prjspreln0  43730  lsmfgcl  44169  kercvrlsm  44178  unxpwdom3  44190  hbt  44225  oa0suclim  44370  om0suclim  44371  oe0suclim  44372  naddcnff  44457  cvgdvgrat  45390  climinf  46711  clim2f  46739  clim2cf  46753  clim0cf  46757  clim2f2  46773  fmtnofac2lem  48746  ovmpordxf  49544  oppcthinendcALT  50669  cotsqcscsq  51023  aacllem  51107