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  3014  ralimdvva  3185  reximdvva  3186  2ralbidva  3200  2rexbidva  3201  2ralbida  3261  spcimgft  3515  copsexgw  5452  copsexg  5453  pofun  5566  imainss  6129  fvmptdf  6976  eqfnfv2  7006  fnex  7193  f1elima  7240  fliftfun  7289  isores2  7310  f1oiso  7328  ovmpodxf  7541  sorpssuni  7710  sorpssint  7711  tfindsg2  7840  2ndconst  8082  poxp2  8124  sexp3  8134  poseq  8139  oalim  8498  omlim  8499  oaass  8527  omlimcl  8544  omass  8546  oelim2  8561  oeoa  8563  oeoelem  8564  nnaass  8588  omabs  8617  eroveu  8787  sbthlem4  9059  fimaxg  9240  fisupg  9241  fofinf1o  9289  fiming  9457  fiinfg  9458  ordtypelem7  9483  hartogs  9503  card2on  9513  unwdomg  9543  wemapwe  9656  frmin  9708  dfac5  10088  cfsmolem  10229  isf32lem2  10313  ttukeylem6  10473  ondomon  10522  alephreg  10541  ltexprlem6  11000  recexsrlem  11062  wloglei  11716  recextlem2  11815  fimaxre  12133  creur  12181  uz11  12824  xrmaxeq  13145  xrmineq  13146  xaddf  13190  xaddass  13215  xleadd1a  13219  xlt2add  13226  xmullem  13230  xmulgt0  13249  xmulasslem3  13252  xlemul1a  13254  xadddilem  13260  fzrevral  13579  seqcaopr2  14009  expnlbnd2  14205  faclbnd4lem4  14267  hashgt23el  14395  rtrclreclem3  15032  rtrclreclem4  15033  relexpindlem  15035  rtrclind  15037  shftlem  15040  01sqrex  15221  cau3lem  15327  limsupbnd2  15455  clim2  15476  clim2c  15477  clim0c  15479  rlimresb  15537  2clim  15544  climabs0  15557  climcn1  15564  climcn2  15565  o1rlimmul  15591  climsqz  15613  climsqz2  15614  rlimsqzlem  15621  lo1le  15624  climsup  15642  caucvgrlem2  15647  iseralt  15657  summolem2  15688  fsum2dlem  15742  cvgcmp  15788  cvgcmpce  15790  climfsum  15792  fsumiun  15793  geomulcvg  15848  mertenslem2  15857  mertens  15858  prodfn0  15866  prodfrec  15867  zprod  15909  fprodeq0  15947  fprodn0  15951  fprod2dlem  15952  smu01lem  16461  gcdcllem1  16475  dvdssq  16543  lcmdvds  16584  coprmdvds2  16630  pclem  16815  pcge0  16839  pcgcd1  16854  prmpwdvds  16881  1arithlem4  16903  4sqlem18  16939  vdwlem10  16967  vdwlem11  16968  ramval  16985  ramub1lem2  17004  ramcl  17006  imasaddfnlem  17497  imasaddflem  17499  imasvscafn  17506  imasleval  17510  ismon2  17702  isepi2  17709  issubc3  17817  cofucl  17856  setcmon  18055  setcepi  18056  ipodrsfi  18504  ipodrsima  18506  isacs3lem  18507  grpidpropd  18595  grprida  18608  gsumpropd2lem  18612  mgmhmpropd  18631  mgmhmima  18648  mhmpropd  18725  mhmimalem  18757  grplcan  18938  dfgrp3lem  18976  mulgdirlem  19043  subgmulg  19078  issubg4  19083  subgint  19088  ssnmz  19104  cycsubgcl  19144  gastacl  19247  orbsta  19251  cntzsubg  19277  galactghm  19340  odmulg  19492  odbezout  19494  sylow3lem2  19564  lsmsubm  19589  efgsfo  19675  mulgmhm  19763  mulgghm  19764  gsumval3  19843  gsumcllem  19844  gsumpt  19898  gsum2d  19908  gsum2d2  19910  prdsgsum  19917  subgdmdprd  19972  dprd2d2  19982  ablfac1eu  20011  rngpropd  20089  srglmhm  20136  srgrmhm  20137  ringpropd  20203  ringlghm  20227  dvdsrpropd  20331  rhmimasubrnglem  20480  cntzsdrg  20717  abvpropd  20750  islmodd  20778  lmodprop2d  20836  lsssubg  20869  lsspropd  20930  lmhmima  20960  lidlsubg  21139  phlpropd  21570  frlmsslsp  21711  lindfmm  21742  islindf4  21753  assapropd  21787  asclpropd  21812  psrass1lem  21847  mplcoe1  21950  mplcoe5  21953  mplind  21983  evlslem2  21992  evlsval  21999  coe1tmmul2  22168  mamuass  22295  mavmulass  22442  mdetuni0  22514  mdetmul  22516  cpmatacl  22609  cpmadugsumfi  22770  cpmadumatpolylem1  22774  cpmadumatpolylem2  22775  cpmadumatpoly  22776  cayhamlem4  22781  neips  23006  neindisj  23010  ordtrest2lem  23096  lmbrf  23153  lmss  23191  isreg2  23270  lmmo  23273  hauscmplem  23299  bwth  23303  2ndcomap  23351  1stcelcls  23354  restlly  23376  islly2  23377  cldllycmp  23388  comppfsc  23425  1stckgenlem  23446  txbas  23460  txbasval  23499  tx1cn  23502  ptpjopn  23505  ptcnp  23515  txnlly  23530  txlm  23541  xkococn  23553  fgabs  23772  fmfnfmlem4  23850  flimcf  23875  hauspwpwf1  23880  fclsbas  23914  fclscf  23918  flimfnfcls  23921  ghmcnp  24008  tsmsxp  24048  isxmet2d  24221  elmopn2  24339  mopni3  24388  blsscls2  24398  metequiv2  24404  metss2lem  24405  met2ndci  24416  metrest  24418  metcnp  24435  metcnp2  24436  metcnpi3  24440  txmetcnp  24441  nmolb2d  24612  xrge0tsms  24729  metdsre  24748  metnrmlem3  24756  fsumcn  24767  elcncf2  24789  mulc1cncf  24804  cncfco  24806  cncfmet  24808  bndth  24863  evth  24864  copco  24924  pcopt2  24929  pcoass  24930  pcorevlem  24932  lmmcvg  25167  lmmbrf  25168  iscau4  25185  iscauf  25186  cmetcaulem  25194  iscmet3lem3  25196  iscmet3lem1  25197  causs  25204  equivcfil  25205  lmclim  25209  caubl  25214  caublcls  25215  bcth3  25237  ivthle  25363  ivthle2  25364  ovoliunlem1  25409  ovolicc2lem5  25428  volsuplem  25462  uniioombllem6  25495  dyaddisjlem  25502  dyadmax  25505  volcn  25513  mbfmulc2lem  25554  ismbf3d  25561  mbfsup  25571  mbfinf  25572  mbflim  25575  i1fmullem  25601  itg2seq  25649  itg2uba  25650  itg2splitlem  25655  itg2split  25656  itg2monolem1  25657  bddiblnc  25749  ditgsplitlem  25767  ellimc2  25784  ellimc3  25786  limcflf  25788  limcmpt  25790  limcco  25800  lhop1lem  25924  dvfsumle  25932  dvfsumleOLD  25933  dvfsumabs  25935  dvfsumrlim  25944  ftc1a  25950  ftc1lem6  25954  mdegmullem  25989  elply2  26107  plypf1  26123  ulmcaulem  26309  ulmcau  26310  ulmss  26312  ulmdvlem3  26317  mtest  26319  itgulm  26323  abelthlem8  26355  abelth  26357  tanord  26453  cxpcn3lem  26663  mcubic  26763  cubic2  26764  dvdsflsumcom  27104  fsumdvdsmul  27111  fsumdvdsmulOLD  27113  lgsdchrval  27271  2sqlem9  27344  rplogsumlem2  27402  rpvmasumlem  27404  dchrvmasumlem1  27412  vmalogdivsum2  27455  logsqvma  27459  selberg  27465  selberg4  27478  pntibndlem3  27509  pntlem3  27526  pntleml  27528  padicabv  27547  padicabvf  27548  padicabvcxp  27549  ostth3  27555  nosupbnd1lem5  27630  noinfbnd1lem5  27645  nocvxminlem  27695  lrrecfr  27856  addsprop  27889  mulsproplem9  28033  mulsproplem12  28036  mulsproplem13  28037  mulsproplem14  28038  mulsprop  28039  slemuld  28047  mulsuniflem  28058  mulsasslem3  28074  axpasch  28874  axcontlem7  28903  axcontlem10  28906  cusgrsize2inds  29387  grpolcan  30465  nvmul0or  30585  nmosetre  30699  blocnilem  30739  blocni  30740  h2hcau  30914  h2hlm  30915  shsel3  31250  chscllem2  31573  homulcl  31694  adjsym  31768  cnvadj  31827  hhcno  31839  hhcnf  31840  lnopl  31849  unoplin  31855  counop  31856  lnfnl  31866  hmoplin  31877  hmopm  31956  nmcexi  31961  lnconi  31968  riesz3i  31997  leopmuli  32068  leopmul  32069  hstle  32165  mdsl0  32245  mdslmd1lem2  32261  atcvatlem  32320  chirredi  32329  cdj1i  32368  sbc2iedf  32400  foresf1o  32439  suppovss  32610  isoun  32631  difioo  32711  swrdf1  32884  xrge0tsmsd  33008  cycpmrn  33106  ressply1invg  33544  ply1unit  33550  fedgmullem2  33632  pstmxmet  33893  ordtrest2NEWlem  33918  esum2dlem  34088  esum2d  34089  dya2icoseg2  34275  eulerpartlemgc  34359  eulerpartlemgh  34375  eulerpartlemgs2  34377  ballotlemimin  34503  signstfvneq0  34569  hgt750lemb  34653  connpconn  35222  cvmliftmolem2  35269  cvmliftlem6  35277  cvmliftlem8  35279  cvmlift2lem12  35301  elmrsubrn  35507  dfon2lem6  35771  ifscgr  36027  brsegle  36091  neibastop2lem  36343  bj-elabd2ALT  36908  bj-ismooredr2  37093  curf  37587  finixpnum  37594  fin2solem  37595  fin2so  37596  lindsenlbs  37604  matunitlindflem1  37605  matunitlindflem2  37606  matunitlindf  37607  poimirlem3  37612  poimirlem4  37613  poimirlem6  37615  poimirlem7  37616  poimirlem14  37623  poimirlem16  37625  poimirlem19  37628  poimirlem22  37631  poimirlem28  37637  poimirlem29  37638  poimirlem30  37639  poimir  37642  heicant  37644  itg2gt0cn  37664  ftc1cnnc  37681  ftc1anclem5  37686  ftc1anclem6  37687  ftc1anclem7  37688  ftc1anc  37690  cover2  37704  filbcmb  37729  fdc  37734  fdc1  37735  seqpo  37736  incsequz  37737  incsequz2  37738  metf1o  37744  lmclim2  37747  geomcau  37748  isbnd2  37772  bndss  37775  ismtybndlem  37795  heibor1lem  37798  rrncmslem  37821  rrnequiv  37824  exidreslem  37866  ghomco  37880  isdrngo3  37948  rngoisocnv  37970  isidlc  38004  idlnegcl  38011  divrngidl  38017  intidl  38018  unichnidl  38020  keridl  38021  igenmin  38053  prnc  38056  ispridlc  38059  erimeq2  38665  prter3  38870  glbconxN  39367  atltcvr  39424  3dim1  39456  lvolnle3at  39571  linepsubN  39741  osumclN  39956  pexmidALTN  39967  lhpmatb  40020  cdlemg1idlemN  40561  dihlss  41239  dihglblem5aN  41281  dihatlat  41323  aks6d1c1p1  42090  aks6d1c5lem1  42119  unitscyglem4  42181  f1o2d2  42216  pwsgprod  42525  selvvvval  42566  fsuppind  42571  fsuppssindlem1  42572  prjspertr  42586  prjspreln0  42590  lsmfgcl  43056  kercvrlsm  43065  unxpwdom3  43077  hbt  43112  oa0suclim  43257  om0suclim  43258  oe0suclim  43259  naddcnff  43344  cvgdvgrat  44295  climinf  45597  clim2f  45627  clim2cf  45641  clim0cf  45645  clim2f2  45661  fmtnofac2lem  47559  ovmpordxf  48317  oppcthinendcALT  49420  cotsqcscsq  49741  aacllem  49780