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  3020  ralimdvva  3184  reximdvva  3185  2ralbidva  3199  2rexbidva  3200  2ralbida  3260  spcimgft  3491  copsexgwOLD  5444  copsexg  5445  pofun  5557  imainss  6118  fvmptdf  6954  eqfnfv2  6984  fnex  7172  f1elima  7218  fliftfun  7267  isores2  7288  f1oiso  7306  ovmpodxf  7517  sorpssuni  7686  sorpssint  7687  tfindsg2  7813  2ndconst  8051  poxp2  8093  sexp3  8103  poseq  8108  oalim  8467  omlim  8468  oaass  8496  omlimcl  8513  omass  8515  oelim2  8531  oeoa  8533  oeoelem  8534  nnaass  8558  omabs  8587  eroveu  8759  sbthlem4  9028  fimaxg  9197  fisupg  9198  fofinf1o  9242  fiming  9413  fiinfg  9414  ordtypelem7  9439  hartogs  9459  card2on  9469  unwdomg  9499  wemapwe  9618  frmin  9673  dfac5  10051  cfsmolem  10192  isf32lem2  10276  ttukeylem6  10436  ondomon  10485  alephreg  10505  ltexprlem6  10964  recexsrlem  11026  wloglei  11682  recextlem2  11781  fimaxre  12100  creur  12153  uz11  12813  xrmaxeq  13131  xrmineq  13132  xaddf  13176  xaddass  13201  xleadd1a  13205  xlt2add  13212  xmullem  13216  xmulgt0  13235  xmulasslem3  13238  xlemul1a  13240  xadddilem  13246  fzrevral  13566  seqcaopr2  14000  expnlbnd2  14196  faclbnd4lem4  14258  hashgt23el  14386  rtrclreclem3  15022  rtrclreclem4  15023  relexpindlem  15025  rtrclind  15027  shftlem  15030  01sqrex  15211  cau3lem  15317  limsupbnd2  15445  clim2  15466  clim2c  15467  clim0c  15469  rlimresb  15527  2clim  15534  climabs0  15547  climcn1  15554  climcn2  15555  o1rlimmul  15581  climsqz  15603  climsqz2  15604  rlimsqzlem  15611  lo1le  15614  climsup  15632  caucvgrlem2  15637  iseralt  15647  summolem2  15678  fsum2dlem  15732  cvgcmp  15779  cvgcmpce  15781  climfsum  15783  fsumiun  15784  geomulcvg  15841  mertenslem2  15850  mertens  15851  prodfn0  15859  prodfrec  15860  zprod  15902  fprodeq0  15940  fprodn0  15944  fprod2dlem  15945  smu01lem  16454  gcdcllem1  16468  dvdssq  16536  lcmdvds  16577  coprmdvds2  16623  pclem  16809  pcge0  16833  pcgcd1  16848  prmpwdvds  16875  1arithlem4  16897  4sqlem18  16933  vdwlem10  16961  vdwlem11  16962  ramval  16979  ramub1lem2  16998  ramcl  17000  imasaddfnlem  17492  imasaddflem  17494  imasvscafn  17501  imasleval  17505  ismon2  17701  isepi2  17708  issubc3  17816  cofucl  17855  setcmon  18054  setcepi  18055  ipodrsfi  18505  ipodrsima  18507  isacs3lem  18508  grpidpropd  18630  grprida  18643  gsumpropd2lem  18647  mgmhmpropd  18666  mgmhmima  18683  mhmpropd  18760  mhmimalem  18792  grplcan  18976  dfgrp3lem  19014  mulgdirlem  19081  subgmulg  19116  issubg4  19121  subgint  19126  ssnmz  19141  cycsubgcl  19181  gastacl  19284  orbsta  19288  cntzsubg  19314  galactghm  19379  odmulg  19531  odbezout  19533  sylow3lem2  19603  lsmsubm  19628  efgsfo  19714  mulgmhm  19802  mulgghm  19803  gsumval3  19882  gsumcllem  19883  gsumpt  19937  gsum2d  19947  gsum2d2  19949  prdsgsum  19956  subgdmdprd  20011  dprd2d2  20021  ablfac1eu  20050  rngpropd  20155  srglmhm  20202  srgrmhm  20203  ringpropd  20269  ringlghm  20293  pwsgprod  20309  dvdsrpropd  20396  rhmimasubrnglem  20542  cntzsdrg  20779  abvpropd  20812  islmodd  20861  lmodprop2d  20919  lsssubg  20952  lsspropd  21012  lmhmima  21042  lidlsubg  21221  phlpropd  21635  frlmsslsp  21776  lindfmm  21807  islindf4  21818  assapropd  21851  asclpropd  21877  psrass1lem  21912  mplcoe1  22015  mplcoe5  22018  mplind  22048  evlslem2  22057  evlsval  22064  coe1tmmul2  22241  mamuass  22367  mavmulass  22514  mdetuni0  22586  mdetmul  22588  cpmatacl  22681  cpmadugsumfi  22842  cpmadumatpolylem1  22846  cpmadumatpolylem2  22847  cpmadumatpoly  22848  cayhamlem4  22853  neips  23078  neindisj  23082  ordtrest2lem  23168  lmbrf  23225  lmss  23263  isreg2  23342  lmmo  23345  hauscmplem  23371  bwth  23375  2ndcomap  23423  1stcelcls  23426  restlly  23448  islly2  23449  cldllycmp  23460  comppfsc  23497  1stckgenlem  23518  txbas  23532  txbasval  23571  tx1cn  23574  ptpjopn  23577  ptcnp  23587  txnlly  23602  txlm  23613  xkococn  23625  fgabs  23844  fmfnfmlem4  23922  flimcf  23947  hauspwpwf1  23952  fclsbas  23986  fclscf  23990  flimfnfcls  23993  ghmcnp  24080  tsmsxp  24120  isxmet2d  24292  elmopn2  24410  mopni3  24459  blsscls2  24469  metequiv2  24475  metss2lem  24476  met2ndci  24487  metrest  24489  metcnp  24506  metcnp2  24507  metcnpi3  24511  txmetcnp  24512  nmolb2d  24683  xrge0tsms  24800  metdsre  24819  metnrmlem3  24827  fsumcn  24837  elcncf2  24857  mulc1cncf  24872  cncfco  24874  cncfmet  24876  bndth  24925  evth  24926  copco  24985  pcopt2  24990  pcoass  24991  pcorevlem  24993  lmmcvg  25228  lmmbrf  25229  iscau4  25246  iscauf  25247  cmetcaulem  25255  iscmet3lem3  25257  iscmet3lem1  25258  causs  25265  equivcfil  25266  lmclim  25270  caubl  25275  caublcls  25276  bcth3  25298  ivthle  25423  ivthle2  25424  ovoliunlem1  25469  ovolicc2lem5  25488  volsuplem  25522  uniioombllem6  25555  dyaddisjlem  25562  dyadmax  25565  volcn  25573  mbfmulc2lem  25614  ismbf3d  25621  mbfsup  25631  mbfinf  25632  mbflim  25635  i1fmullem  25661  itg2seq  25709  itg2uba  25710  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  bddiblnc  25809  ditgsplitlem  25827  ellimc2  25844  ellimc3  25846  limcflf  25848  limcmpt  25850  limcco  25860  lhop1lem  25980  dvfsumle  25988  dvfsumabs  25990  dvfsumrlim  25998  ftc1a  26004  ftc1lem6  26008  mdegmullem  26043  elply2  26161  plypf1  26177  ulmcaulem  26359  ulmcau  26360  ulmss  26362  ulmdvlem3  26367  mtest  26369  itgulm  26373  abelthlem8  26404  abelth  26406  tanord  26502  cxpcn3lem  26711  mcubic  26811  cubic2  26812  dvdsflsumcom  27151  fsumdvdsmul  27158  lgsdchrval  27317  2sqlem9  27390  rplogsumlem2  27448  rpvmasumlem  27450  dchrvmasumlem1  27458  vmalogdivsum2  27501  logsqvma  27505  selberg  27511  selberg4  27524  pntibndlem3  27555  pntlem3  27572  pntleml  27574  padicabv  27593  padicabvf  27594  padicabvcxp  27595  ostth3  27601  nosupbnd1lem5  27676  noinfbnd1lem5  27691  nocvxminlem  27746  lrrecfr  27935  addsprop  27968  mulsproplem9  28116  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  mulsprop  28122  lemulsd  28130  mulsuniflem  28141  mulsasslem3  28157  axpasch  29010  axcontlem7  29039  axcontlem10  29042  cusgrsize2inds  29522  grpolcan  30601  nvmul0or  30721  nmosetre  30835  blocnilem  30875  blocni  30876  h2hcau  31050  h2hlm  31051  shsel3  31386  chscllem2  31709  homulcl  31830  adjsym  31904  cnvadj  31963  hhcno  31975  hhcnf  31976  lnopl  31985  unoplin  31991  counop  31992  lnfnl  32002  hmoplin  32013  hmopm  32092  nmcexi  32097  lnconi  32104  riesz3i  32133  leopmuli  32204  leopmul  32205  hstle  32301  mdsl0  32381  mdslmd1lem2  32397  atcvatlem  32456  chirredi  32465  cdj1i  32504  sbc2iedf  32534  foresf1o  32574  suppovss  32754  isoun  32775  difioo  32855  swrdf1  33016  xrge0tsmsd  33134  cycpmrn  33204  ressply1invg  33629  ply1unit  33635  fedgmullem2  33774  pstmxmet  34041  ordtrest2NEWlem  34066  esum2dlem  34236  esum2d  34237  dya2icoseg2  34422  eulerpartlemgc  34506  eulerpartlemgh  34522  eulerpartlemgs2  34524  ballotlemimin  34650  signstfvneq0  34716  hgt750lemb  34800  connpconn  35417  cvmliftmolem2  35464  cvmliftlem6  35472  cvmliftlem8  35474  cvmlift2lem12  35496  elmrsubrn  35702  dfon2lem6  35968  ifscgr  36226  brsegle  36290  neibastop2lem  36542  bj-elabd2ALT  37232  bj-ismooredr2  37422  curf  37919  finixpnum  37926  fin2solem  37927  fin2so  37928  lindsenlbs  37936  matunitlindflem1  37937  matunitlindflem2  37938  matunitlindf  37939  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem14  37955  poimirlem16  37957  poimirlem19  37960  poimirlem22  37963  poimirlem28  37969  poimirlem29  37970  poimirlem30  37971  poimir  37974  heicant  37976  itg2gt0cn  37996  ftc1cnnc  38013  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anc  38022  cover2  38036  filbcmb  38061  fdc  38066  fdc1  38067  seqpo  38068  incsequz  38069  incsequz2  38070  metf1o  38076  lmclim2  38079  geomcau  38080  isbnd2  38104  bndss  38107  ismtybndlem  38127  heibor1lem  38130  rrncmslem  38153  rrnequiv  38156  exidreslem  38198  ghomco  38212  isdrngo3  38280  rngoisocnv  38302  isidlc  38336  idlnegcl  38343  divrngidl  38349  intidl  38350  unichnidl  38352  keridl  38353  igenmin  38385  prnc  38388  ispridlc  38391  erimeq2  39084  prter3  39328  glbconxN  39824  atltcvr  39881  3dim1  39913  lvolnle3at  40028  linepsubN  40198  osumclN  40413  pexmidALTN  40424  lhpmatb  40477  cdlemg1idlemN  41018  dihlss  41696  dihglblem5aN  41738  dihatlat  41780  aks6d1c1p1  42546  aks6d1c5lem1  42575  unitscyglem4  42637  f1o2d2  42674  selvvvval  43018  fsuppind  43023  fsuppssindlem1  43024  prjspertr  43038  prjspreln0  43042  lsmfgcl  43502  kercvrlsm  43511  unxpwdom3  43523  hbt  43558  oa0suclim  43703  om0suclim  43704  oe0suclim  43705  naddcnff  43790  cvgdvgrat  44740  climinf  46036  clim2f  46064  clim2cf  46078  clim0cf  46082  clim2f2  46098  fmtnofac2lem  48031  ovmpordxf  48815  oppcthinendcALT  49916  cotsqcscsq  50237  aacllem  50276