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  814  pm2.61dda  815  pm2.61da2ne  3027  ralimdvva  3203  reximdvva  3204  2ralbidva  3216  2rexbidva  3217  2ralbida  3280  spcimgft  3545  copsexgw  5500  copsexg  5501  pofun  5614  imainss  6175  fvmptdf  7021  eqfnfv2  7051  fnex  7236  f1elima  7282  fliftfun  7331  isores2  7352  f1oiso  7370  ovmpodxf  7582  sorpssuni  7750  sorpssint  7751  tfindsg2  7882  2ndconst  8124  poxp2  8166  sexp3  8176  poseq  8181  oalim  8568  omlim  8569  oaass  8597  omlimcl  8614  omass  8616  oelim2  8631  oeoa  8633  oeoelem  8634  nnaass  8658  omabs  8687  eroveu  8850  sbthlem4  9124  fimaxg  9320  fisupg  9321  fofinf1o  9369  fiming  9535  fiinfg  9536  ordtypelem7  9561  hartogs  9581  card2on  9591  unwdomg  9621  wemapwe  9734  frmin  9786  dfac5  10166  cfsmolem  10307  isf32lem2  10391  ttukeylem6  10551  ondomon  10600  alephreg  10619  ltexprlem6  11078  recexsrlem  11140  wloglei  11792  recextlem2  11891  fimaxre  12209  creur  12257  uz11  12900  xrmaxeq  13217  xrmineq  13218  xaddf  13262  xaddass  13287  xleadd1a  13291  xlt2add  13298  xmullem  13302  xmulgt0  13321  xmulasslem3  13324  xlemul1a  13326  xadddilem  13332  fzrevral  13648  seqcaopr2  14075  expnlbnd2  14269  faclbnd4lem4  14331  hashgt23el  14459  rtrclreclem3  15095  rtrclreclem4  15096  relexpindlem  15098  rtrclind  15100  shftlem  15103  01sqrex  15284  cau3lem  15389  limsupbnd2  15515  clim2  15536  clim2c  15537  clim0c  15539  rlimresb  15597  2clim  15604  climabs0  15617  climcn1  15624  climcn2  15625  o1rlimmul  15651  climsqz  15673  climsqz2  15674  rlimsqzlem  15681  lo1le  15684  climsup  15702  caucvgrlem2  15707  iseralt  15717  summolem2  15748  fsum2dlem  15802  cvgcmp  15848  cvgcmpce  15850  climfsum  15852  fsumiun  15853  geomulcvg  15908  mertenslem2  15917  mertens  15918  prodfn0  15926  prodfrec  15927  zprod  15969  fprodeq0  16007  fprodn0  16011  fprod2dlem  16012  smu01lem  16518  gcdcllem1  16532  dvdssq  16600  lcmdvds  16641  coprmdvds2  16687  pclem  16871  pcge0  16895  pcgcd1  16910  prmpwdvds  16937  1arithlem4  16959  4sqlem18  16995  vdwlem10  17023  vdwlem11  17024  ramval  17041  ramub1lem2  17060  ramcl  17062  imasaddfnlem  17574  imasaddflem  17576  imasvscafn  17583  imasleval  17587  ismon2  17781  isepi2  17788  issubc3  17899  cofucl  17938  setcmon  18140  setcepi  18141  ipodrsfi  18596  ipodrsima  18598  isacs3lem  18599  grpidpropd  18687  grprida  18700  gsumpropd2lem  18704  mgmhmpropd  18723  mgmhmima  18740  mhmpropd  18817  mhmimalem  18849  grplcan  19030  dfgrp3lem  19068  mulgdirlem  19135  subgmulg  19170  issubg4  19175  subgint  19180  ssnmz  19196  cycsubgcl  19236  gastacl  19339  orbsta  19343  cntzsubg  19369  galactghm  19436  odmulg  19588  odbezout  19590  sylow3lem2  19660  lsmsubm  19685  efgsfo  19771  mulgmhm  19859  mulgghm  19860  gsumval3  19939  gsumcllem  19940  gsumpt  19994  gsum2d  20004  gsum2d2  20006  prdsgsum  20013  subgdmdprd  20068  dprd2d2  20078  ablfac1eu  20107  rngpropd  20191  srglmhm  20238  srgrmhm  20239  ringpropd  20301  ringlghm  20325  dvdsrpropd  20432  rhmimasubrnglem  20581  cntzsdrg  20819  abvpropd  20852  islmodd  20880  lmodprop2d  20938  lsssubg  20972  lsspropd  21033  lmhmima  21063  lidlsubg  21250  phlpropd  21690  frlmsslsp  21833  lindfmm  21864  islindf4  21875  assapropd  21909  asclpropd  21934  psrass1lem  21969  mplcoe1  22072  mplcoe5  22075  mplind  22111  evlslem2  22120  evlsval  22127  coe1tmmul2  22294  mamuass  22421  mavmulass  22570  mdetuni0  22642  mdetmul  22644  cpmatacl  22737  cpmadugsumfi  22898  cpmadumatpolylem1  22902  cpmadumatpolylem2  22903  cpmadumatpoly  22904  cayhamlem4  22909  neips  23136  neindisj  23140  ordtrest2lem  23226  lmbrf  23283  lmss  23321  isreg2  23400  lmmo  23403  hauscmplem  23429  bwth  23433  2ndcomap  23481  1stcelcls  23484  restlly  23506  islly2  23507  cldllycmp  23518  comppfsc  23555  1stckgenlem  23576  txbas  23590  txbasval  23629  tx1cn  23632  ptpjopn  23635  ptcnp  23645  txnlly  23660  txlm  23671  xkococn  23683  fgabs  23902  fmfnfmlem4  23980  flimcf  24005  hauspwpwf1  24010  fclsbas  24044  fclscf  24048  flimfnfcls  24051  ghmcnp  24138  tsmsxp  24178  isxmet2d  24352  elmopn2  24470  mopni3  24522  blsscls2  24532  metequiv2  24538  metss2lem  24539  met2ndci  24550  metrest  24552  metcnp  24569  metcnp2  24570  metcnpi3  24574  txmetcnp  24575  nmolb2d  24754  xrge0tsms  24869  metdsre  24888  metnrmlem3  24896  fsumcn  24907  elcncf2  24929  mulc1cncf  24944  cncfco  24946  cncfmet  24948  bndth  25003  evth  25004  copco  25064  pcopt2  25069  pcoass  25070  pcorevlem  25072  lmmcvg  25308  lmmbrf  25309  iscau4  25326  iscauf  25327  cmetcaulem  25335  iscmet3lem3  25337  iscmet3lem1  25338  causs  25345  equivcfil  25346  lmclim  25350  caubl  25355  caublcls  25356  bcth3  25378  ivthle  25504  ivthle2  25505  ovoliunlem1  25550  ovolicc2lem5  25569  volsuplem  25603  uniioombllem6  25636  dyaddisjlem  25643  dyadmax  25646  volcn  25654  mbfmulc2lem  25695  ismbf3d  25702  mbfsup  25712  mbfinf  25713  mbflim  25716  i1fmullem  25742  itg2seq  25791  itg2uba  25792  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  bddiblnc  25891  ditgsplitlem  25909  ellimc2  25926  ellimc3  25928  limcflf  25930  limcmpt  25932  limcco  25942  lhop1lem  26066  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumrlim  26086  ftc1a  26092  ftc1lem6  26096  mdegmullem  26131  elply2  26249  plypf1  26265  ulmcaulem  26451  ulmcau  26452  ulmss  26454  ulmdvlem3  26459  mtest  26461  itgulm  26465  abelthlem8  26497  abelth  26499  tanord  26594  cxpcn3lem  26804  mcubic  26904  cubic2  26905  dvdsflsumcom  27245  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  lgsdchrval  27412  2sqlem9  27485  rplogsumlem2  27543  rpvmasumlem  27545  dchrvmasumlem1  27553  vmalogdivsum2  27596  logsqvma  27600  selberg  27606  selberg4  27619  pntibndlem3  27650  pntlem3  27667  pntleml  27669  padicabv  27688  padicabvf  27689  padicabvcxp  27690  ostth3  27696  nosupbnd1lem5  27771  noinfbnd1lem5  27786  nocvxminlem  27836  lrrecfr  27990  addsprop  28023  mulsproplem9  28164  mulsproplem12  28167  mulsproplem13  28168  mulsproplem14  28169  mulsprop  28170  slemuld  28178  mulsuniflem  28189  mulsasslem3  28205  axpasch  28970  axcontlem7  28999  axcontlem10  29002  cusgrsize2inds  29485  grpolcan  30558  nvmul0or  30678  nmosetre  30792  blocnilem  30832  blocni  30833  h2hcau  31007  h2hlm  31008  shsel3  31343  chscllem2  31666  homulcl  31787  adjsym  31861  cnvadj  31920  hhcno  31932  hhcnf  31933  lnopl  31942  unoplin  31948  counop  31949  lnfnl  31959  hmoplin  31970  hmopm  32049  nmcexi  32054  lnconi  32061  riesz3i  32090  leopmuli  32161  leopmul  32162  hstle  32258  mdsl0  32338  mdslmd1lem2  32354  atcvatlem  32413  chirredi  32422  cdj1i  32461  sbc2iedf  32493  foresf1o  32531  suppovss  32695  isoun  32716  difioo  32790  swrdf1  32925  xrge0tsmsd  33047  cycpmrn  33145  ressply1invg  33573  ply1unit  33579  fedgmullem2  33657  pstmxmet  33857  ordtrest2NEWlem  33882  esum2dlem  34072  esum2d  34073  dya2icoseg2  34259  eulerpartlemgc  34343  eulerpartlemgh  34359  eulerpartlemgs2  34361  ballotlemimin  34486  signstfvneq0  34565  hgt750lemb  34649  connpconn  35219  cvmliftmolem2  35266  cvmliftlem6  35274  cvmliftlem8  35276  cvmlift2lem12  35298  elmrsubrn  35504  dfon2lem6  35769  ifscgr  36025  brsegle  36089  neibastop2lem  36342  bj-elabd2ALT  36907  bj-ismooredr2  37092  curf  37584  finixpnum  37591  fin2solem  37592  fin2so  37593  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  matunitlindf  37604  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem14  37620  poimirlem16  37622  poimirlem19  37625  poimirlem22  37628  poimirlem28  37634  poimirlem29  37635  poimirlem30  37636  poimir  37639  heicant  37641  itg2gt0cn  37661  ftc1cnnc  37678  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anc  37687  cover2  37701  filbcmb  37726  fdc  37731  fdc1  37732  seqpo  37733  incsequz  37734  incsequz2  37735  metf1o  37741  lmclim2  37744  geomcau  37745  isbnd2  37769  bndss  37772  ismtybndlem  37792  heibor1lem  37795  rrncmslem  37818  rrnequiv  37821  exidreslem  37863  ghomco  37877  isdrngo3  37945  rngoisocnv  37967  isidlc  38001  idlnegcl  38008  divrngidl  38014  intidl  38015  unichnidl  38017  keridl  38018  igenmin  38050  prnc  38053  ispridlc  38056  erimeq2  38659  prter3  38863  glbconxN  39360  atltcvr  39417  3dim1  39449  lvolnle3at  39564  linepsubN  39734  osumclN  39949  pexmidALTN  39960  lhpmatb  40013  cdlemg1idlemN  40554  dihlss  41232  dihglblem5aN  41274  dihatlat  41316  aks6d1c1p1  42088  aks6d1c5lem1  42117  unitscyglem4  42179  metakunt1  42186  metakunt2  42187  f1o2d2  42252  pwsgprod  42530  selvvvval  42571  fsuppind  42576  fsuppssindlem1  42577  prjspertr  42591  prjspreln0  42595  lsmfgcl  43062  kercvrlsm  43071  unxpwdom3  43083  hbt  43118  oa0suclim  43264  om0suclim  43265  oe0suclim  43266  naddcnff  43351  cvgdvgrat  44308  climinf  45561  clim2f  45591  clim2cf  45605  clim0cf  45609  clim2f2  45625  fmtnofac2lem  47492  ovmpordxf  48183  cotsqcscsq  48992  aacllem  49031