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  3021  ralimdvva  3192  reximdvva  3193  2ralbidva  3207  2rexbidva  3208  2ralbida  3269  spcimgft  3530  copsexgw  5470  copsexg  5471  pofun  5584  imainss  6148  fvmptdf  6997  eqfnfv2  7027  fnex  7214  f1elima  7261  fliftfun  7310  isores2  7331  f1oiso  7349  ovmpodxf  7562  sorpssuni  7731  sorpssint  7732  tfindsg2  7862  2ndconst  8105  poxp2  8147  sexp3  8157  poseq  8162  oalim  8549  omlim  8550  oaass  8578  omlimcl  8595  omass  8597  oelim2  8612  oeoa  8614  oeoelem  8615  nnaass  8639  omabs  8668  eroveu  8831  sbthlem4  9105  fimaxg  9300  fisupg  9301  fofinf1o  9349  fiming  9517  fiinfg  9518  ordtypelem7  9543  hartogs  9563  card2on  9573  unwdomg  9603  wemapwe  9716  frmin  9768  dfac5  10148  cfsmolem  10289  isf32lem2  10373  ttukeylem6  10533  ondomon  10582  alephreg  10601  ltexprlem6  11060  recexsrlem  11122  wloglei  11774  recextlem2  11873  fimaxre  12191  creur  12239  uz11  12882  xrmaxeq  13200  xrmineq  13201  xaddf  13245  xaddass  13270  xleadd1a  13274  xlt2add  13281  xmullem  13285  xmulgt0  13304  xmulasslem3  13307  xlemul1a  13309  xadddilem  13315  fzrevral  13634  seqcaopr2  14061  expnlbnd2  14257  faclbnd4lem4  14319  hashgt23el  14447  rtrclreclem3  15084  rtrclreclem4  15085  relexpindlem  15087  rtrclind  15089  shftlem  15092  01sqrex  15273  cau3lem  15378  limsupbnd2  15504  clim2  15525  clim2c  15526  clim0c  15528  rlimresb  15586  2clim  15593  climabs0  15606  climcn1  15613  climcn2  15614  o1rlimmul  15640  climsqz  15662  climsqz2  15663  rlimsqzlem  15670  lo1le  15673  climsup  15691  caucvgrlem2  15696  iseralt  15706  summolem2  15737  fsum2dlem  15791  cvgcmp  15837  cvgcmpce  15839  climfsum  15841  fsumiun  15842  geomulcvg  15897  mertenslem2  15906  mertens  15907  prodfn0  15915  prodfrec  15916  zprod  15958  fprodeq0  15996  fprodn0  16000  fprod2dlem  16001  smu01lem  16509  gcdcllem1  16523  dvdssq  16591  lcmdvds  16632  coprmdvds2  16678  pclem  16863  pcge0  16887  pcgcd1  16902  prmpwdvds  16929  1arithlem4  16951  4sqlem18  16987  vdwlem10  17015  vdwlem11  17016  ramval  17033  ramub1lem2  17052  ramcl  17054  imasaddfnlem  17547  imasaddflem  17549  imasvscafn  17556  imasleval  17560  ismon2  17752  isepi2  17759  issubc3  17867  cofucl  17906  setcmon  18105  setcepi  18106  ipodrsfi  18554  ipodrsima  18556  isacs3lem  18557  grpidpropd  18645  grprida  18658  gsumpropd2lem  18662  mgmhmpropd  18681  mgmhmima  18698  mhmpropd  18775  mhmimalem  18807  grplcan  18988  dfgrp3lem  19026  mulgdirlem  19093  subgmulg  19128  issubg4  19133  subgint  19138  ssnmz  19154  cycsubgcl  19194  gastacl  19297  orbsta  19301  cntzsubg  19327  galactghm  19390  odmulg  19542  odbezout  19544  sylow3lem2  19614  lsmsubm  19639  efgsfo  19725  mulgmhm  19813  mulgghm  19814  gsumval3  19893  gsumcllem  19894  gsumpt  19948  gsum2d  19958  gsum2d2  19960  prdsgsum  19967  subgdmdprd  20022  dprd2d2  20032  ablfac1eu  20061  rngpropd  20139  srglmhm  20186  srgrmhm  20187  ringpropd  20253  ringlghm  20277  dvdsrpropd  20381  rhmimasubrnglem  20530  cntzsdrg  20767  abvpropd  20800  islmodd  20828  lmodprop2d  20886  lsssubg  20919  lsspropd  20980  lmhmima  21010  lidlsubg  21189  phlpropd  21620  frlmsslsp  21761  lindfmm  21792  islindf4  21803  assapropd  21837  asclpropd  21862  psrass1lem  21897  mplcoe1  22000  mplcoe5  22003  mplind  22033  evlslem2  22042  evlsval  22049  coe1tmmul2  22218  mamuass  22345  mavmulass  22492  mdetuni0  22564  mdetmul  22566  cpmatacl  22659  cpmadugsumfi  22820  cpmadumatpolylem1  22824  cpmadumatpolylem2  22825  cpmadumatpoly  22826  cayhamlem4  22831  neips  23056  neindisj  23060  ordtrest2lem  23146  lmbrf  23203  lmss  23241  isreg2  23320  lmmo  23323  hauscmplem  23349  bwth  23353  2ndcomap  23401  1stcelcls  23404  restlly  23426  islly2  23427  cldllycmp  23438  comppfsc  23475  1stckgenlem  23496  txbas  23510  txbasval  23549  tx1cn  23552  ptpjopn  23555  ptcnp  23565  txnlly  23580  txlm  23591  xkococn  23603  fgabs  23822  fmfnfmlem4  23900  flimcf  23925  hauspwpwf1  23930  fclsbas  23964  fclscf  23968  flimfnfcls  23971  ghmcnp  24058  tsmsxp  24098  isxmet2d  24271  elmopn2  24389  mopni3  24438  blsscls2  24448  metequiv2  24454  metss2lem  24455  met2ndci  24466  metrest  24468  metcnp  24485  metcnp2  24486  metcnpi3  24490  txmetcnp  24491  nmolb2d  24662  xrge0tsms  24779  metdsre  24798  metnrmlem3  24806  fsumcn  24817  elcncf2  24839  mulc1cncf  24854  cncfco  24856  cncfmet  24858  bndth  24913  evth  24914  copco  24974  pcopt2  24979  pcoass  24980  pcorevlem  24982  lmmcvg  25218  lmmbrf  25219  iscau4  25236  iscauf  25237  cmetcaulem  25245  iscmet3lem3  25247  iscmet3lem1  25248  causs  25255  equivcfil  25256  lmclim  25260  caubl  25265  caublcls  25266  bcth3  25288  ivthle  25414  ivthle2  25415  ovoliunlem1  25460  ovolicc2lem5  25479  volsuplem  25513  uniioombllem6  25546  dyaddisjlem  25553  dyadmax  25556  volcn  25564  mbfmulc2lem  25605  ismbf3d  25612  mbfsup  25622  mbfinf  25623  mbflim  25626  i1fmullem  25652  itg2seq  25700  itg2uba  25701  itg2splitlem  25706  itg2split  25707  itg2monolem1  25708  bddiblnc  25800  ditgsplitlem  25818  ellimc2  25835  ellimc3  25837  limcflf  25839  limcmpt  25841  limcco  25851  lhop1lem  25975  dvfsumle  25983  dvfsumleOLD  25984  dvfsumabs  25986  dvfsumrlim  25995  ftc1a  26001  ftc1lem6  26005  mdegmullem  26040  elply2  26158  plypf1  26174  ulmcaulem  26360  ulmcau  26361  ulmss  26363  ulmdvlem3  26368  mtest  26370  itgulm  26374  abelthlem8  26406  abelth  26408  tanord  26504  cxpcn3lem  26714  mcubic  26814  cubic2  26815  dvdsflsumcom  27155  fsumdvdsmul  27162  fsumdvdsmulOLD  27164  lgsdchrval  27322  2sqlem9  27395  rplogsumlem2  27453  rpvmasumlem  27455  dchrvmasumlem1  27463  vmalogdivsum2  27506  logsqvma  27510  selberg  27516  selberg4  27529  pntibndlem3  27560  pntlem3  27577  pntleml  27579  padicabv  27598  padicabvf  27599  padicabvcxp  27600  ostth3  27606  nosupbnd1lem5  27681  noinfbnd1lem5  27696  nocvxminlem  27746  lrrecfr  27907  addsprop  27940  mulsproplem9  28084  mulsproplem12  28087  mulsproplem13  28088  mulsproplem14  28089  mulsprop  28090  slemuld  28098  mulsuniflem  28109  mulsasslem3  28125  axpasch  28925  axcontlem7  28954  axcontlem10  28957  cusgrsize2inds  29438  grpolcan  30516  nvmul0or  30636  nmosetre  30750  blocnilem  30790  blocni  30791  h2hcau  30965  h2hlm  30966  shsel3  31301  chscllem2  31624  homulcl  31745  adjsym  31819  cnvadj  31878  hhcno  31890  hhcnf  31891  lnopl  31900  unoplin  31906  counop  31907  lnfnl  31917  hmoplin  31928  hmopm  32007  nmcexi  32012  lnconi  32019  riesz3i  32048  leopmuli  32119  leopmul  32120  hstle  32216  mdsl0  32296  mdslmd1lem2  32312  atcvatlem  32371  chirredi  32380  cdj1i  32419  sbc2iedf  32451  foresf1o  32490  suppovss  32663  isoun  32684  difioo  32764  swrdf1  32937  xrge0tsmsd  33061  cycpmrn  33159  ressply1invg  33587  ply1unit  33593  fedgmullem2  33675  pstmxmet  33933  ordtrest2NEWlem  33958  esum2dlem  34128  esum2d  34129  dya2icoseg2  34315  eulerpartlemgc  34399  eulerpartlemgh  34415  eulerpartlemgs2  34417  ballotlemimin  34543  signstfvneq0  34609  hgt750lemb  34693  connpconn  35262  cvmliftmolem2  35309  cvmliftlem6  35317  cvmliftlem8  35319  cvmlift2lem12  35341  elmrsubrn  35547  dfon2lem6  35811  ifscgr  36067  brsegle  36131  neibastop2lem  36383  bj-elabd2ALT  36948  bj-ismooredr2  37133  curf  37627  finixpnum  37634  fin2solem  37635  fin2so  37636  lindsenlbs  37644  matunitlindflem1  37645  matunitlindflem2  37646  matunitlindf  37647  poimirlem3  37652  poimirlem4  37653  poimirlem6  37655  poimirlem7  37656  poimirlem14  37663  poimirlem16  37665  poimirlem19  37668  poimirlem22  37671  poimirlem28  37677  poimirlem29  37678  poimirlem30  37679  poimir  37682  heicant  37684  itg2gt0cn  37704  ftc1cnnc  37721  ftc1anclem5  37726  ftc1anclem6  37727  ftc1anclem7  37728  ftc1anc  37730  cover2  37744  filbcmb  37769  fdc  37774  fdc1  37775  seqpo  37776  incsequz  37777  incsequz2  37778  metf1o  37784  lmclim2  37787  geomcau  37788  isbnd2  37812  bndss  37815  ismtybndlem  37835  heibor1lem  37838  rrncmslem  37861  rrnequiv  37864  exidreslem  37906  ghomco  37920  isdrngo3  37988  rngoisocnv  38010  isidlc  38044  idlnegcl  38051  divrngidl  38057  intidl  38058  unichnidl  38060  keridl  38061  igenmin  38093  prnc  38096  ispridlc  38099  erimeq2  38701  prter3  38905  glbconxN  39402  atltcvr  39459  3dim1  39491  lvolnle3at  39606  linepsubN  39776  osumclN  39991  pexmidALTN  40002  lhpmatb  40055  cdlemg1idlemN  40596  dihlss  41274  dihglblem5aN  41316  dihatlat  41358  aks6d1c1p1  42125  aks6d1c5lem1  42154  unitscyglem4  42216  f1o2d2  42251  pwsgprod  42542  selvvvval  42583  fsuppind  42588  fsuppssindlem1  42589  prjspertr  42603  prjspreln0  42607  lsmfgcl  43073  kercvrlsm  43082  unxpwdom3  43094  hbt  43129  oa0suclim  43274  om0suclim  43275  oe0suclim  43276  naddcnff  43361  cvgdvgrat  44312  climinf  45615  clim2f  45645  clim2cf  45659  clim0cf  45663  clim2f2  45679  fmtnofac2lem  47562  ovmpordxf  48294  oppcthinendcALT  49307  cotsqcscsq  49606  aacllem  49645