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  3020  ralimdvva  3183  reximdvva  3184  2ralbidva  3198  2rexbidva  3199  2ralbida  3259  spcimgft  3503  copsexgw  5438  copsexg  5439  pofun  5550  imainss  6112  fvmptdf  6947  eqfnfv2  6977  fnex  7163  f1elima  7209  fliftfun  7258  isores2  7279  f1oiso  7297  ovmpodxf  7508  sorpssuni  7677  sorpssint  7678  tfindsg2  7804  2ndconst  8043  poxp2  8085  sexp3  8095  poseq  8100  oalim  8459  omlim  8460  oaass  8488  omlimcl  8505  omass  8507  oelim2  8523  oeoa  8525  oeoelem  8526  nnaass  8550  omabs  8579  eroveu  8749  sbthlem4  9018  fimaxg  9187  fisupg  9188  fofinf1o  9232  fiming  9403  fiinfg  9404  ordtypelem7  9429  hartogs  9449  card2on  9459  unwdomg  9489  wemapwe  9606  frmin  9661  dfac5  10039  cfsmolem  10180  isf32lem2  10264  ttukeylem6  10424  ondomon  10473  alephreg  10493  ltexprlem6  10952  recexsrlem  11014  wloglei  11669  recextlem2  11768  fimaxre  12086  creur  12139  uz11  12776  xrmaxeq  13094  xrmineq  13095  xaddf  13139  xaddass  13164  xleadd1a  13168  xlt2add  13175  xmullem  13179  xmulgt0  13198  xmulasslem3  13201  xlemul1a  13203  xadddilem  13209  fzrevral  13528  seqcaopr2  13961  expnlbnd2  14157  faclbnd4lem4  14219  hashgt23el  14347  rtrclreclem3  14983  rtrclreclem4  14984  relexpindlem  14986  rtrclind  14988  shftlem  14991  01sqrex  15172  cau3lem  15278  limsupbnd2  15406  clim2  15427  clim2c  15428  clim0c  15430  rlimresb  15488  2clim  15495  climabs0  15508  climcn1  15515  climcn2  15516  o1rlimmul  15542  climsqz  15564  climsqz2  15565  rlimsqzlem  15572  lo1le  15575  climsup  15593  caucvgrlem2  15598  iseralt  15608  summolem2  15639  fsum2dlem  15693  cvgcmp  15739  cvgcmpce  15741  climfsum  15743  fsumiun  15744  geomulcvg  15799  mertenslem2  15808  mertens  15809  prodfn0  15817  prodfrec  15818  zprod  15860  fprodeq0  15898  fprodn0  15902  fprod2dlem  15903  smu01lem  16412  gcdcllem1  16426  dvdssq  16494  lcmdvds  16535  coprmdvds2  16581  pclem  16766  pcge0  16790  pcgcd1  16805  prmpwdvds  16832  1arithlem4  16854  4sqlem18  16890  vdwlem10  16918  vdwlem11  16919  ramval  16936  ramub1lem2  16955  ramcl  16957  imasaddfnlem  17449  imasaddflem  17451  imasvscafn  17458  imasleval  17462  ismon2  17658  isepi2  17665  issubc3  17773  cofucl  17812  setcmon  18011  setcepi  18012  ipodrsfi  18462  ipodrsima  18464  isacs3lem  18465  grpidpropd  18587  grprida  18600  gsumpropd2lem  18604  mgmhmpropd  18623  mgmhmima  18640  mhmpropd  18717  mhmimalem  18749  grplcan  18930  dfgrp3lem  18968  mulgdirlem  19035  subgmulg  19070  issubg4  19075  subgint  19080  ssnmz  19095  cycsubgcl  19135  gastacl  19238  orbsta  19242  cntzsubg  19268  galactghm  19333  odmulg  19485  odbezout  19487  sylow3lem2  19557  lsmsubm  19582  efgsfo  19668  mulgmhm  19756  mulgghm  19757  gsumval3  19836  gsumcllem  19837  gsumpt  19891  gsum2d  19901  gsum2d2  19903  prdsgsum  19910  subgdmdprd  19965  dprd2d2  19975  ablfac1eu  20004  rngpropd  20109  srglmhm  20156  srgrmhm  20157  ringpropd  20223  ringlghm  20247  pwsgprod  20265  dvdsrpropd  20352  rhmimasubrnglem  20498  cntzsdrg  20735  abvpropd  20768  islmodd  20817  lmodprop2d  20875  lsssubg  20908  lsspropd  20969  lmhmima  20999  lidlsubg  21178  phlpropd  21610  frlmsslsp  21751  lindfmm  21782  islindf4  21793  assapropd  21827  asclpropd  21853  psrass1lem  21888  mplcoe1  21992  mplcoe5  21995  mplind  22025  evlslem2  22034  evlsval  22041  coe1tmmul2  22218  mamuass  22346  mavmulass  22493  mdetuni0  22565  mdetmul  22567  cpmatacl  22660  cpmadugsumfi  22821  cpmadumatpolylem1  22825  cpmadumatpolylem2  22826  cpmadumatpoly  22827  cayhamlem4  22832  neips  23057  neindisj  23061  ordtrest2lem  23147  lmbrf  23204  lmss  23242  isreg2  23321  lmmo  23324  hauscmplem  23350  bwth  23354  2ndcomap  23402  1stcelcls  23405  restlly  23427  islly2  23428  cldllycmp  23439  comppfsc  23476  1stckgenlem  23497  txbas  23511  txbasval  23550  tx1cn  23553  ptpjopn  23556  ptcnp  23566  txnlly  23581  txlm  23592  xkococn  23604  fgabs  23823  fmfnfmlem4  23901  flimcf  23926  hauspwpwf1  23931  fclsbas  23965  fclscf  23969  flimfnfcls  23972  ghmcnp  24059  tsmsxp  24099  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  25217  lmmbrf  25218  iscau4  25235  iscauf  25236  cmetcaulem  25244  iscmet3lem3  25246  iscmet3lem1  25247  causs  25254  equivcfil  25255  lmclim  25259  caubl  25264  caublcls  25265  bcth3  25287  ivthle  25413  ivthle2  25414  ovoliunlem1  25459  ovolicc2lem5  25478  volsuplem  25512  uniioombllem6  25545  dyaddisjlem  25552  dyadmax  25555  volcn  25563  mbfmulc2lem  25604  ismbf3d  25611  mbfsup  25621  mbfinf  25622  mbflim  25625  i1fmullem  25651  itg2seq  25699  itg2uba  25700  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  bddiblnc  25799  ditgsplitlem  25817  ellimc2  25834  ellimc3  25836  limcflf  25838  limcmpt  25840  limcco  25850  lhop1lem  25974  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumrlim  25994  ftc1a  26000  ftc1lem6  26004  mdegmullem  26039  elply2  26157  plypf1  26173  ulmcaulem  26359  ulmcau  26360  ulmss  26362  ulmdvlem3  26367  mtest  26369  itgulm  26373  abelthlem8  26405  abelth  26407  tanord  26503  cxpcn3lem  26713  mcubic  26813  cubic2  26814  dvdsflsumcom  27154  fsumdvdsmul  27161  fsumdvdsmulOLD  27163  lgsdchrval  27321  2sqlem9  27394  rplogsumlem2  27452  rpvmasumlem  27454  dchrvmasumlem1  27462  vmalogdivsum2  27505  logsqvma  27509  selberg  27515  selberg4  27528  pntibndlem3  27559  pntlem3  27576  pntleml  27578  padicabv  27597  padicabvf  27598  padicabvcxp  27599  ostth3  27605  nosupbnd1lem5  27680  noinfbnd1lem5  27695  nocvxminlem  27750  lrrecfr  27939  addsprop  27972  mulsproplem9  28120  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  mulsprop  28126  lemulsd  28134  mulsuniflem  28145  mulsasslem3  28161  axpasch  29014  axcontlem7  29043  axcontlem10  29046  cusgrsize2inds  29527  grpolcan  30605  nvmul0or  30725  nmosetre  30839  blocnilem  30879  blocni  30880  h2hcau  31054  h2hlm  31055  shsel3  31390  chscllem2  31713  homulcl  31834  adjsym  31908  cnvadj  31967  hhcno  31979  hhcnf  31980  lnopl  31989  unoplin  31995  counop  31996  lnfnl  32006  hmoplin  32017  hmopm  32096  nmcexi  32101  lnconi  32108  riesz3i  32137  leopmuli  32208  leopmul  32209  hstle  32305  mdsl0  32385  mdslmd1lem2  32401  atcvatlem  32460  chirredi  32469  cdj1i  32508  sbc2iedf  32539  foresf1o  32579  suppovss  32760  isoun  32781  difioo  32862  swrdf1  33038  xrge0tsmsd  33155  cycpmrn  33225  ressply1invg  33650  ply1unit  33656  fedgmullem2  33787  pstmxmet  34054  ordtrest2NEWlem  34079  esum2dlem  34249  esum2d  34250  dya2icoseg2  34435  eulerpartlemgc  34519  eulerpartlemgh  34535  eulerpartlemgs2  34537  ballotlemimin  34663  signstfvneq0  34729  hgt750lemb  34813  connpconn  35429  cvmliftmolem2  35476  cvmliftlem6  35484  cvmliftlem8  35486  cvmlift2lem12  35508  elmrsubrn  35714  dfon2lem6  35980  ifscgr  36238  brsegle  36302  neibastop2lem  36554  bj-elabd2ALT  37126  bj-ismooredr2  37311  curf  37795  finixpnum  37802  fin2solem  37803  fin2so  37804  lindsenlbs  37812  matunitlindflem1  37813  matunitlindflem2  37814  matunitlindf  37815  poimirlem3  37820  poimirlem4  37821  poimirlem6  37823  poimirlem7  37824  poimirlem14  37831  poimirlem16  37833  poimirlem19  37836  poimirlem22  37839  poimirlem28  37845  poimirlem29  37846  poimirlem30  37847  poimir  37850  heicant  37852  itg2gt0cn  37872  ftc1cnnc  37889  ftc1anclem5  37894  ftc1anclem6  37895  ftc1anclem7  37896  ftc1anc  37898  cover2  37912  filbcmb  37937  fdc  37942  fdc1  37943  seqpo  37944  incsequz  37945  incsequz2  37946  metf1o  37952  lmclim2  37955  geomcau  37956  isbnd2  37980  bndss  37983  ismtybndlem  38003  heibor1lem  38006  rrncmslem  38029  rrnequiv  38032  exidreslem  38074  ghomco  38088  isdrngo3  38156  rngoisocnv  38178  isidlc  38212  idlnegcl  38219  divrngidl  38225  intidl  38226  unichnidl  38228  keridl  38229  igenmin  38261  prnc  38264  ispridlc  38267  erimeq2  38933  prter3  39138  glbconxN  39634  atltcvr  39691  3dim1  39723  lvolnle3at  39838  linepsubN  40008  osumclN  40223  pexmidALTN  40234  lhpmatb  40287  cdlemg1idlemN  40828  dihlss  41506  dihglblem5aN  41548  dihatlat  41590  aks6d1c1p1  42357  aks6d1c5lem1  42386  unitscyglem4  42448  f1o2d2  42485  selvvvval  42824  fsuppind  42829  fsuppssindlem1  42830  prjspertr  42844  prjspreln0  42848  lsmfgcl  43312  kercvrlsm  43321  unxpwdom3  43333  hbt  43368  oa0suclim  43513  om0suclim  43514  oe0suclim  43515  naddcnff  43600  cvgdvgrat  44550  climinf  45848  clim2f  45876  clim2cf  45890  clim0cf  45894  clim2f2  45910  fmtnofac2lem  47810  ovmpordxf  48581  oppcthinendcALT  49682  cotsqcscsq  50003  aacllem  50042