Theorem anassrs 471

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 424	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 421	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anass  472  anass1rs  654  anabss5  667  anabss7  672  mpanr1  702  pm2.61ddan  813  pm2.61dda  814  pm2.61da2ne  3075  ralimdvva  3146  2ralbidva  3163  2ralbida  3196  reximdvva  3236  2rexbidva  3258  copsexgw  5346  copsexg  5347  pofun  5455  imainss  5978  fvmptdf  6751  eqfnfv2  6780  fnex  6957  f1elima  6999  fliftfun  7044  isores2  7065  f1oiso  7083  ovmpodxf  7279  sorpssuni  7438  sorpssint  7439  tfindsg2  7556  2ndconst  7779  oalim  8140  omlim  8141  oaass  8170  omlimcl  8187  omass  8189  oelim2  8204  oeoa  8206  oeoelem  8207  nnaass  8231  omabs  8257  eroveu  8375  sbthlem4  8614  fimaxg  8749  fisupg  8750  fofinf1o  8783  fiming  8946  fiinfg  8947  ordtypelem7  8972  hartogs  8992  card2on  9002  unwdomg  9032  wemapwe  9144  dfac5  9539  cfsmolem  9681  isf32lem2  9765  ttukeylem6  9925  ondomon  9974  alephreg  9993  ltexprlem6  10452  recexsrlem  10514  wloglei  11161  recextlem2  11260  fimaxre  11573  creur  11619  uz11  12255  xrmaxeq  12560  xrmineq  12561  xaddf  12605  xaddass  12630  xleadd1a  12634  xlt2add  12641  xmullem  12645  xmulgt0  12664  xmulasslem3  12667  xlemul1a  12669  xadddilem  12675  fzrevral  12987  seqcaopr2  13402  expnlbnd2  13591  faclbnd4lem4  13652  hashgt23el  13781  rtrclreclem3  14411  rtrclreclem4  14412  relexpindlem  14414  rtrclind  14416  shftlem  14419  01sqrex  14601  cau3lem  14706  limsupbnd2  14832  clim2  14853  clim2c  14854  clim0c  14856  rlimresb  14914  2clim  14921  climabs0  14934  climcn1  14940  climcn2  14941  o1rlimmul  14967  climsqz  14989  climsqz2  14990  rlimsqzlem  14997  lo1le  15000  climsup  15018  caucvgrlem2  15023  iseralt  15033  summolem2  15065  fsum2dlem  15117  cvgcmp  15163  cvgcmpce  15165  climfsum  15167  fsumiun  15168  geomulcvg  15224  mertenslem2  15233  mertens  15234  prodfn0  15242  prodfrec  15243  zprod  15283  fprodeq0  15321  fprodn0  15325  fprod2dlem  15326  smu01lem  15824  gcdcllem1  15838  gcdmultiplezOLD  15891  dvdssq  15901  lcmdvds  15942  coprmdvds2  15988  pclem  16165  pcge0  16188  pcgcd1  16203  prmpwdvds  16230  1arithlem4  16252  4sqlem18  16288  vdwlem10  16316  vdwlem11  16317  ramval  16334  ramub1lem2  16353  ramcl  16355  imasaddfnlem  16793  imasaddflem  16795  imasvscafn  16802  imasleval  16806  ismon2  16996  isepi2  17003  issubc3  17111  cofucl  17150  setcmon  17339  setcepi  17340  ipodrsfi  17765  ipodrsima  17767  isacs3lem  17768  grpidpropd  17864  grpridd  17877  gsumpropd2lem  17881  mhmpropd  17954  mhmima  17981  gsumccatOLD  17997  grplcan  18153  dfgrp3lem  18189  mulgdirlem  18250  subgmulg  18285  issubg4  18290  subgint  18295  ssnmz  18310  cycsubgcl  18341  gastacl  18431  orbsta  18435  cntzsubg  18459  galactghm  18524  odmulg  18675  odbezout  18677  sylow3lem2  18745  lsmsubm  18770  efgsfo  18857  mulgmhm  18941  mulgghm  18942  gsumval3  19020  gsumcllem  19021  gsumpt  19075  gsum2d  19085  gsum2d2  19087  prdsgsum  19094  subgdmdprd  19149  dprd2d2  19159  ablfac1eu  19188  srglmhm  19278  srgrmhm  19279  ringpropd  19328  ringlghm  19350  dvdsrpropd  19442  cntzsdrg  19574  abvpropd  19606  islmodd  19633  lmodprop2d  19689  lsssubg  19722  lsspropd  19782  lmhmima  19812  lidlsubg  19981  phlpropd  20344  frlmsslsp  20485  lindfmm  20516  islindf4  20527  assapropd  20558  asclpropd  20583  psrass1lem  20615  mplcoe1  20705  mplcoe5  20708  mplind  20741  evlslem2  20751  evlsval  20758  coe1tmmul2  20905  mamuass  21007  mavmulass  21154  mdetuni0  21226  mdetmul  21228  cpmatacl  21321  cpmadugsumfi  21482  cpmadumatpolylem1  21486  cpmadumatpolylem2  21487  cpmadumatpoly  21488  cayhamlem4  21493  neips  21718  neindisj  21722  ordtrest2lem  21808  lmbrf  21865  lmss  21903  isreg2  21982  lmmo  21985  hauscmplem  22011  bwth  22015  2ndcomap  22063  1stcelcls  22066  restlly  22088  islly2  22089  cldllycmp  22100  comppfsc  22137  1stckgenlem  22158  txbas  22172  txbasval  22211  tx1cn  22214  ptpjopn  22217  ptcnp  22227  txnlly  22242  txlm  22253  xkococn  22265  fgabs  22484  fmfnfmlem4  22562  flimcf  22587  hauspwpwf1  22592  fclsbas  22626  fclscf  22630  flimfnfcls  22633  ghmcnp  22720  tsmsxp  22760  isxmet2d  22934  elmopn2  23052  mopni3  23101  blsscls2  23111  metequiv2  23117  metss2lem  23118  met2ndci  23129  metrest  23131  metcnp  23148  metcnp2  23149  metcnpi3  23153  txmetcnp  23154  nmolb2d  23324  xrge0tsms  23439  metdsre  23458  metnrmlem3  23466  fsumcn  23475  elcncf2  23495  mulc1cncf  23510  cncfco  23512  cncfmet  23514  bndth  23563  evth  23564  copco  23623  pcopt2  23628  pcoass  23629  pcorevlem  23631  lmmcvg  23865  lmmbrf  23866  iscau4  23883  iscauf  23884  cmetcaulem  23892  iscmet3lem3  23894  iscmet3lem1  23895  causs  23902  equivcfil  23903  lmclim  23907  caubl  23912  caublcls  23913  bcth3  23935  ivthle  24060  ivthle2  24061  ovoliunlem1  24106  ovolicc2lem5  24125  volsuplem  24159  uniioombllem6  24192  dyaddisjlem  24199  dyadmax  24202  volcn  24210  mbfmulc2lem  24251  ismbf3d  24258  mbfsup  24268  mbfinf  24269  mbflim  24272  i1fmullem  24298  itg2seq  24346  itg2uba  24347  itg2splitlem  24352  itg2split  24353  itg2monolem1  24354  bddiblnc  24445  ditgsplitlem  24463  ellimc2  24480  ellimc3  24482  limcflf  24484  limcmpt  24486  limcco  24496  lhop1lem  24616  dvfsumle  24624  dvfsumabs  24626  dvfsumrlim  24634  ftc1a  24640  ftc1lem6  24644  mdegmullem  24679  elply2  24793  plypf1  24809  ulmcaulem  24989  ulmcau  24990  ulmss  24992  ulmdvlem3  24997  mtest  24999  itgulm  25003  abelthlem8  25034  abelth  25036  tanord  25130  cxpcn3lem  25336  mcubic  25433  cubic2  25434  dvdsflsumcom  25773  fsumdvdsmul  25780  lgsdchrval  25938  2sqlem9  26011  rplogsumlem2  26069  rpvmasumlem  26071  dchrvmasumlem1  26079  vmalogdivsum2  26122  logsqvma  26126  selberg  26132  selberg4  26145  pntibndlem3  26176  pntlem3  26193  pntleml  26195  padicabv  26214  padicabvf  26215  padicabvcxp  26216  ostth3  26222  axpasch  26735  axcontlem7  26764  axcontlem10  26767  cusgrsize2inds  27243  grpolcan  28313  nvmul0or  28433  nmosetre  28547  blocnilem  28587  blocni  28588  h2hcau  28762  h2hlm  28763  shsel3  29098  chscllem2  29421  homulcl  29542  adjsym  29616  cnvadj  29675  hhcno  29687  hhcnf  29688  lnopl  29697  unoplin  29703  counop  29704  lnfnl  29714  hmoplin  29725  hmopm  29804  nmcexi  29809  lnconi  29816  riesz3i  29845  leopmuli  29916  leopmul  29917  hstle  30013  mdsl0  30093  mdslmd1lem2  30109  atcvatlem  30168  chirredi  30177  cdj1i  30216  sbc2iedf  30237  foresf1o  30273  suppovss  30443  isoun  30461  difioo  30531  swrdf1  30656  xrge0tsmsd  30742  cycpmrn  30835  fedgmullem2  31114  pstmxmet  31250  ordtrest2NEWlem  31275  esum2dlem  31461  esum2d  31462  dya2icoseg2  31646  eulerpartlemgc  31730  eulerpartlemgh  31746  eulerpartlemgs2  31748  ballotlemimin  31873  signstfvneq0  31952  hgt750lemb  32037  connpconn  32595  cvmliftmolem2  32642  cvmliftlem6  32650  cvmliftlem8  32652  cvmlift2lem12  32674  elmrsubrn  32880  dfon2lem6  33146  poseq  33208  nosupbnd1lem5  33325  nocvxminlem  33360  ifscgr  33618  brsegle  33682  neibastop2lem  33821  bj-ismooredr2  34525  curf  35035  finixpnum  35042  fin2solem  35043  fin2so  35044  lindsenlbs  35052  matunitlindflem1  35053  matunitlindflem2  35054  matunitlindf  35055  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem14  35071  poimirlem16  35073  poimirlem19  35076  poimirlem22  35079  poimirlem28  35085  poimirlem29  35086  poimirlem30  35087  poimir  35090  heicant  35092  itg2gt0cn  35112  ftc1cnnc  35129  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anc  35138  cover2  35152  filbcmb  35178  fdc  35183  fdc1  35184  seqpo  35185  incsequz  35186  incsequz2  35187  metf1o  35193  lmclim2  35196  geomcau  35197  isbnd2  35221  bndss  35224  ismtybndlem  35244  heibor1lem  35247  rrncmslem  35270  rrnequiv  35273  exidreslem  35315  ghomco  35329  isdrngo3  35397  rngoisocnv  35419  isidlc  35453  idlnegcl  35460  divrngidl  35466  intidl  35467  unichnidl  35469  keridl  35470  igenmin  35502  prnc  35505  ispridlc  35508  erim2  36071  prter3  36178  glbconxN  36674  atltcvr  36731  3dim1  36763  lvolnle3at  36878  linepsubN  37048  osumclN  37263  pexmidALTN  37274  lhpmatb  37327  cdlemg1idlemN  37868  dihlss  38546  dihglblem5aN  38588  dihatlat  38630  metakunt1  39350  metakunt2  39351  fsuppind  39456  fsuppssindlem1  39457  prjspertr  39599  prjspreln0  39603  lsmfgcl  40018  kercvrlsm  40027  unxpwdom3  40039  hbt  40074  cvgdvgrat  41017  climinf  42248  clim2f  42278  clim2cf  42292  clim0cf  42296  clim2f2  42312  fmtnofac2lem  44085  isomuspgrlem2d  44349  mgmhmpropd  44405  mgmhmima  44422  ovmpordxf  44740  cotsqcscsq  45288  aacllem  45329