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  655  anabss5  668  anabss7  673  mpanr1  703  pm2.61ddan  813  pm2.61dda  814  pm2.61da2ne  3016  ralimdvva  3179  reximdvva  3180  2ralbidva  3194  2rexbidva  3195  2ralbida  3255  spcimgft  3501  copsexgw  5430  copsexg  5431  pofun  5542  imainss  6101  fvmptdf  6935  eqfnfv2  6965  fnex  7151  f1elima  7197  fliftfun  7246  isores2  7267  f1oiso  7285  ovmpodxf  7496  sorpssuni  7665  sorpssint  7666  tfindsg2  7792  2ndconst  8031  poxp2  8073  sexp3  8083  poseq  8088  oalim  8447  omlim  8448  oaass  8476  omlimcl  8493  omass  8495  oelim2  8510  oeoa  8512  oeoelem  8513  nnaass  8537  omabs  8566  eroveu  8736  sbthlem4  9003  fimaxg  9171  fisupg  9172  fofinf1o  9216  fiming  9384  fiinfg  9385  ordtypelem7  9410  hartogs  9430  card2on  9440  unwdomg  9470  wemapwe  9587  frmin  9639  dfac5  10017  cfsmolem  10158  isf32lem2  10242  ttukeylem6  10402  ondomon  10451  alephreg  10470  ltexprlem6  10929  recexsrlem  10991  wloglei  11646  recextlem2  11745  fimaxre  12063  creur  12116  uz11  12754  xrmaxeq  13075  xrmineq  13076  xaddf  13120  xaddass  13145  xleadd1a  13149  xlt2add  13156  xmullem  13160  xmulgt0  13179  xmulasslem3  13182  xlemul1a  13184  xadddilem  13190  fzrevral  13509  seqcaopr2  13942  expnlbnd2  14138  faclbnd4lem4  14200  hashgt23el  14328  rtrclreclem3  14964  rtrclreclem4  14965  relexpindlem  14967  rtrclind  14969  shftlem  14972  01sqrex  15153  cau3lem  15259  limsupbnd2  15387  clim2  15408  clim2c  15409  clim0c  15411  rlimresb  15469  2clim  15476  climabs0  15489  climcn1  15496  climcn2  15497  o1rlimmul  15523  climsqz  15545  climsqz2  15546  rlimsqzlem  15553  lo1le  15556  climsup  15574  caucvgrlem2  15579  iseralt  15589  summolem2  15620  fsum2dlem  15674  cvgcmp  15720  cvgcmpce  15722  climfsum  15724  fsumiun  15725  geomulcvg  15780  mertenslem2  15789  mertens  15790  prodfn0  15798  prodfrec  15799  zprod  15841  fprodeq0  15879  fprodn0  15883  fprod2dlem  15884  smu01lem  16393  gcdcllem1  16407  dvdssq  16475  lcmdvds  16516  coprmdvds2  16562  pclem  16747  pcge0  16771  pcgcd1  16786  prmpwdvds  16813  1arithlem4  16835  4sqlem18  16871  vdwlem10  16899  vdwlem11  16900  ramval  16917  ramub1lem2  16936  ramcl  16938  imasaddfnlem  17429  imasaddflem  17431  imasvscafn  17438  imasleval  17442  ismon2  17638  isepi2  17645  issubc3  17753  cofucl  17792  setcmon  17991  setcepi  17992  ipodrsfi  18442  ipodrsima  18444  isacs3lem  18445  grpidpropd  18567  grprida  18580  gsumpropd2lem  18584  mgmhmpropd  18603  mgmhmima  18620  mhmpropd  18697  mhmimalem  18729  grplcan  18910  dfgrp3lem  18948  mulgdirlem  19015  subgmulg  19050  issubg4  19055  subgint  19060  ssnmz  19076  cycsubgcl  19116  gastacl  19219  orbsta  19223  cntzsubg  19249  galactghm  19314  odmulg  19466  odbezout  19468  sylow3lem2  19538  lsmsubm  19563  efgsfo  19649  mulgmhm  19737  mulgghm  19738  gsumval3  19817  gsumcllem  19818  gsumpt  19872  gsum2d  19882  gsum2d2  19884  prdsgsum  19891  subgdmdprd  19946  dprd2d2  19956  ablfac1eu  19985  rngpropd  20090  srglmhm  20137  srgrmhm  20138  ringpropd  20204  ringlghm  20228  dvdsrpropd  20332  rhmimasubrnglem  20478  cntzsdrg  20715  abvpropd  20748  islmodd  20797  lmodprop2d  20855  lsssubg  20888  lsspropd  20949  lmhmima  20979  lidlsubg  21158  phlpropd  21590  frlmsslsp  21731  lindfmm  21762  islindf4  21773  assapropd  21807  asclpropd  21832  psrass1lem  21867  mplcoe1  21970  mplcoe5  21973  mplind  22003  evlslem2  22012  evlsval  22019  coe1tmmul2  22188  mamuass  22315  mavmulass  22462  mdetuni0  22534  mdetmul  22536  cpmatacl  22629  cpmadugsumfi  22790  cpmadumatpolylem1  22794  cpmadumatpolylem2  22795  cpmadumatpoly  22796  cayhamlem4  22801  neips  23026  neindisj  23030  ordtrest2lem  23116  lmbrf  23173  lmss  23211  isreg2  23290  lmmo  23293  hauscmplem  23319  bwth  23323  2ndcomap  23371  1stcelcls  23374  restlly  23396  islly2  23397  cldllycmp  23408  comppfsc  23445  1stckgenlem  23466  txbas  23480  txbasval  23519  tx1cn  23522  ptpjopn  23525  ptcnp  23535  txnlly  23550  txlm  23561  xkococn  23573  fgabs  23792  fmfnfmlem4  23870  flimcf  23895  hauspwpwf1  23900  fclsbas  23934  fclscf  23938  flimfnfcls  23941  ghmcnp  24028  tsmsxp  24068  isxmet2d  24240  elmopn2  24358  mopni3  24407  blsscls2  24417  metequiv2  24423  metss2lem  24424  met2ndci  24435  metrest  24437  metcnp  24454  metcnp2  24455  metcnpi3  24459  txmetcnp  24460  nmolb2d  24631  xrge0tsms  24748  metdsre  24767  metnrmlem3  24775  fsumcn  24786  elcncf2  24808  mulc1cncf  24823  cncfco  24825  cncfmet  24827  bndth  24882  evth  24883  copco  24943  pcopt2  24948  pcoass  24949  pcorevlem  24951  lmmcvg  25186  lmmbrf  25187  iscau4  25204  iscauf  25205  cmetcaulem  25213  iscmet3lem3  25215  iscmet3lem1  25216  causs  25223  equivcfil  25224  lmclim  25228  caubl  25233  caublcls  25234  bcth3  25256  ivthle  25382  ivthle2  25383  ovoliunlem1  25428  ovolicc2lem5  25447  volsuplem  25481  uniioombllem6  25514  dyaddisjlem  25521  dyadmax  25524  volcn  25532  mbfmulc2lem  25573  ismbf3d  25580  mbfsup  25590  mbfinf  25591  mbflim  25594  i1fmullem  25620  itg2seq  25668  itg2uba  25669  itg2splitlem  25674  itg2split  25675  itg2monolem1  25676  bddiblnc  25768  ditgsplitlem  25786  ellimc2  25803  ellimc3  25805  limcflf  25807  limcmpt  25809  limcco  25819  lhop1lem  25943  dvfsumle  25951  dvfsumleOLD  25952  dvfsumabs  25954  dvfsumrlim  25963  ftc1a  25969  ftc1lem6  25973  mdegmullem  26008  elply2  26126  plypf1  26142  ulmcaulem  26328  ulmcau  26329  ulmss  26331  ulmdvlem3  26336  mtest  26338  itgulm  26342  abelthlem8  26374  abelth  26376  tanord  26472  cxpcn3lem  26682  mcubic  26782  cubic2  26783  dvdsflsumcom  27123  fsumdvdsmul  27130  fsumdvdsmulOLD  27132  lgsdchrval  27290  2sqlem9  27363  rplogsumlem2  27421  rpvmasumlem  27423  dchrvmasumlem1  27431  vmalogdivsum2  27474  logsqvma  27478  selberg  27484  selberg4  27497  pntibndlem3  27528  pntlem3  27545  pntleml  27547  padicabv  27566  padicabvf  27567  padicabvcxp  27568  ostth3  27574  nosupbnd1lem5  27649  noinfbnd1lem5  27664  nocvxminlem  27715  lrrecfr  27884  addsprop  27917  mulsproplem9  28061  mulsproplem12  28064  mulsproplem13  28065  mulsproplem14  28066  mulsprop  28067  slemuld  28075  mulsuniflem  28086  mulsasslem3  28102  axpasch  28917  axcontlem7  28946  axcontlem10  28949  cusgrsize2inds  29430  grpolcan  30505  nvmul0or  30625  nmosetre  30739  blocnilem  30779  blocni  30780  h2hcau  30954  h2hlm  30955  shsel3  31290  chscllem2  31613  homulcl  31734  adjsym  31808  cnvadj  31867  hhcno  31879  hhcnf  31880  lnopl  31889  unoplin  31895  counop  31896  lnfnl  31906  hmoplin  31917  hmopm  31996  nmcexi  32001  lnconi  32008  riesz3i  32037  leopmuli  32108  leopmul  32109  hstle  32205  mdsl0  32285  mdslmd1lem2  32301  atcvatlem  32360  chirredi  32369  cdj1i  32408  sbc2iedf  32439  foresf1o  32479  suppovss  32657  isoun  32678  difioo  32760  swrdf1  32932  xrge0tsmsd  33037  cycpmrn  33107  ressply1invg  33527  ply1unit  33533  fedgmullem2  33638  pstmxmet  33905  ordtrest2NEWlem  33930  esum2dlem  34100  esum2d  34101  dya2icoseg2  34286  eulerpartlemgc  34370  eulerpartlemgh  34386  eulerpartlemgs2  34388  ballotlemimin  34514  signstfvneq0  34580  hgt750lemb  34664  connpconn  35267  cvmliftmolem2  35314  cvmliftlem6  35322  cvmliftlem8  35324  cvmlift2lem12  35346  elmrsubrn  35552  dfon2lem6  35821  ifscgr  36077  brsegle  36141  neibastop2lem  36393  bj-elabd2ALT  36958  bj-ismooredr2  37143  curf  37637  finixpnum  37644  fin2solem  37645  fin2so  37646  lindsenlbs  37654  matunitlindflem1  37655  matunitlindflem2  37656  matunitlindf  37657  poimirlem3  37662  poimirlem4  37663  poimirlem6  37665  poimirlem7  37666  poimirlem14  37673  poimirlem16  37675  poimirlem19  37678  poimirlem22  37681  poimirlem28  37687  poimirlem29  37688  poimirlem30  37689  poimir  37692  heicant  37694  itg2gt0cn  37714  ftc1cnnc  37731  ftc1anclem5  37736  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anc  37740  cover2  37754  filbcmb  37779  fdc  37784  fdc1  37785  seqpo  37786  incsequz  37787  incsequz2  37788  metf1o  37794  lmclim2  37797  geomcau  37798  isbnd2  37822  bndss  37825  ismtybndlem  37845  heibor1lem  37848  rrncmslem  37871  rrnequiv  37874  exidreslem  37916  ghomco  37930  isdrngo3  37998  rngoisocnv  38020  isidlc  38054  idlnegcl  38061  divrngidl  38067  intidl  38068  unichnidl  38070  keridl  38071  igenmin  38103  prnc  38106  ispridlc  38109  erimeq2  38715  prter3  38920  glbconxN  39416  atltcvr  39473  3dim1  39505  lvolnle3at  39620  linepsubN  39790  osumclN  40005  pexmidALTN  40016  lhpmatb  40069  cdlemg1idlemN  40610  dihlss  41288  dihglblem5aN  41330  dihatlat  41372  aks6d1c1p1  42139  aks6d1c5lem1  42168  unitscyglem4  42230  f1o2d2  42265  pwsgprod  42576  selvvvval  42617  fsuppind  42622  fsuppssindlem1  42623  prjspertr  42637  prjspreln0  42641  lsmfgcl  43106  kercvrlsm  43115  unxpwdom3  43127  hbt  43162  oa0suclim  43307  om0suclim  43308  oe0suclim  43309  naddcnff  43394  cvgdvgrat  44345  climinf  45645  clim2f  45673  clim2cf  45687  clim0cf  45691  clim2f2  45707  fmtnofac2lem  47598  ovmpordxf  48369  oppcthinendcALT  49472  cotsqcscsq  49793  aacllem  49832