Theorem anassrs 472

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  anass  473  anass1rs  667  anabss5  680  anabss7  685  mpanr1  715  pm2.61ddan  825  pm2.61dda  826  pm2.61da2ne  3048  ralimdvva  3212  reximdvva  3213  2ralbidva  3227  2rexbidva  3228  2ralbida  3288  spcimgft  3517  copsexgwOLD  5463  copsexg  5464  pofun  5577  imainss  6142  fvmptdf  6986  eqfnfv2  7016  fnex  7205  f1elima  7251  fliftfun  7300  isores2  7321  f1oiso  7339  ovmpodxf  7550  sorpssuni  7719  sorpssint  7720  tfindsg2  7846  2ndconst  8084  mpof1o2d  8109  poxp2  8127  sexp3  8137  poseq  8142  oalim  8505  omlim  8506  oaass  8534  omlimcl  8551  omass  8553  oelim2  8569  oeoa  8571  oeoelem  8572  nnaass  8596  omabs  8625  eroveu  8798  sbthlem4  9066  fimaxg  9235  fisupg  9236  fofinf1o  9277  fiming  9448  fiinfg  9449  ordtypelem7  9474  hartogs  9494  card2on  9504  unwdomg  9534  wemapwe  9654  frmin  9709  dfac5  10100  cfsmolem  10242  isf32lem2  10326  ttukeylem6  10486  ondomon  10535  alephreg  10555  ltexprlem6  11014  recexsrlem  11076  wloglei  11734  recextlem2  11833  fimaxre  12147  creur  12200  uz11  12875  xrmaxeq  13193  xrmineq  13194  xaddf  13238  xaddass  13263  xleadd1a  13267  xlt2add  13274  xmullem  13278  xmulgt0  13297  xmulasslem3  13300  xlemul1a  13302  xadddilem  13308  fzrevral  13628  seqcaopr2  14062  expnlbnd2  14258  faclbnd4lem4  14320  hashgt23el  14449  rtrclreclem3  15085  rtrclreclem4  15086  relexpindlem  15088  rtrclind  15090  shftlem  15093  01sqrex  15288  cau3lem  15394  limsupbnd2  15522  clim2  15543  clim2c  15544  clim0c  15546  rlimresb  15604  2clim  15611  climabs0  15624  climcn1  15631  climcn2  15632  o1rlimmul  15658  climsqz  15680  climsqz2  15681  rlimsqzlem  15688  lo1le  15691  climsup  15709  caucvgrlem2  15714  iseralt  15724  summolem2  15755  fsum2dlem  15809  cvgcmp  15856  cvgcmpce  15858  climfsum  15860  fsumiun  15861  geomulcvg  15918  mertenslem2  15927  mertens  15928  prodfn0  15936  prodfrec  15937  zprod  15979  fprodeq0  16017  fprodn0  16021  fprod2dlem  16022  smu01lem  16531  gcdcllem1  16545  dvdssq  16613  lcmdvds  16654  coprmdvds2  16700  pclem  16886  pcge0  16910  pcgcd1  16925  prmpwdvds  16952  1arithlem4  16974  4sqlem18  17010  vdwlem10  17038  vdwlem11  17039  ramval  17056  ramub1lem2  17075  ramcl  17077  imasaddfnlem  17570  imasaddflem  17572  imasvscafn  17579  imasleval  17583  ismon2  17779  isepi2  17786  issubc3  17894  cofucl  17933  setcmon  18132  setcepi  18133  ipodrsfi  18583  ipodrsima  18585  isacs3lem  18586  grpidpropd  18708  grprida  18721  gsumpropd2lem  18725  mgmhmpropd  18744  mgmhmima  18761  mhmpropd  18838  mhmimalem  18871  grplcan  19055  dfgrp3lem  19092  mulgdirlem  19159  subgmulg  19195  issubg4  19200  subgint  19205  ssnmz  19220  cycsubgcl  19265  gastacl  19367  orbsta  19371  cntzsubg  19397  galactghm  19462  odmulg  19614  odbezout  19616  sylow3lem2  19686  lsmsubm  19711  efgsfo  19797  mulgmhm  19885  mulgghm  19886  gsumval3  19965  gsumcllem  19966  gsumpt  20020  gsum2d  20030  gsum2d2  20032  prdsgsum  20039  subgdmdprd  20094  dprd2d2  20104  ablfac1eu  20133  rngpropd  20240  srglmhm  20291  srgrmhm  20292  ringpropd  20359  ringlghm  20383  pwsgprod  20399  dvdsrpropd  20486  rhmimasubrnglem  20638  cntzsdrg  20871  abvpropd  20904  islmodd  20953  lmodprop2d  21011  lsssubg  21044  lsspropd  21104  lmhmima  21134  lidlsubg  21314  phlpropd  21762  frlmsslsp  21903  lindfmm  21934  islindf4  21945  assapropd  21978  asclpropd  22004  psrass1lem  22040  mplcoe1  22145  mplcoe5  22148  mplind  22178  evlslem2  22187  evlsval  22194  selvvvval  22250  coe1tmmul2  22394  mamuass  22516  mavmulass  22663  mdetuni0  22735  mdetmul  22737  cpmatacl  22830  cpmadugsumfi  22991  cpmadumatpolylem1  22995  cpmadumatpolylem2  22996  cpmadumatpoly  22997  cayhamlem4  23002  neips  23227  neindisj  23231  ordtrest2lem  23317  lmbrf  23374  lmss  23412  isreg2  23491  lmmo  23494  hauscmplem  23520  bwth  23524  2ndcomap  23572  1stcelcls  23575  restlly  23597  islly2  23598  cldllycmp  23609  comppfsc  23646  1stckgenlem  23667  txbas  23681  txbasval  23720  tx1cn  23723  ptpjopn  23726  ptcnp  23736  txnlly  23751  txlm  23762  xkococn  23774  fgabs  23993  fmfnfmlem4  24071  flimcf  24096  hauspwpwf1  24101  fclsbas  24135  fclscf  24139  flimfnfcls  24142  ghmcnp  24229  tsmsxp  24269  isxmet2d  24441  elmopn2  24559  mopni3  24608  blsscls2  24618  metequiv2  24624  metss2lem  24625  met2ndci  24636  metrest  24638  metcnp  24655  metcnp2  24656  metcnpi3  24660  txmetcnp  24661  nmolb2d  24832  xrge0tsms  24949  metdsre  24968  metnrmlem3  24976  fsumcn  24986  elcncf2  25006  mulc1cncf  25021  cncfco  25023  cncfmet  25025  bndth  25074  evth  25075  copco  25134  pcopt2  25139  pcoass  25140  pcorevlem  25142  lmmcvg  25377  lmmbrf  25378  iscau4  25395  iscauf  25396  cmetcaulem  25404  iscmet3lem3  25406  iscmet3lem1  25407  causs  25414  equivcfil  25415  lmclim  25419  caubl  25424  caublcls  25425  bcth3  25447  ivthle  25572  ivthle2  25573  ovoliunlem1  25618  ovolicc2lem5  25637  volsuplem  25671  uniioombllem6  25704  dyaddisjlem  25711  dyadmax  25714  volcn  25722  mbfmulc2lem  25763  ismbf3d  25770  mbfsup  25780  mbfinf  25781  mbflim  25784  i1fmullem  25810  itg2seq  25858  itg2uba  25859  itg2splitlem  25864  itg2split  25865  itg2monolem1  25866  bddiblnc  25958  ditgsplitlem  25976  ellimc2  25993  ellimc3  25995  limcflf  25997  limcmpt  25999  limcco  26009  lhop1lem  26129  dvfsumle  26137  dvfsumabs  26139  dvfsumrlim  26147  ftc1a  26153  ftc1lem6  26157  mdegmullem  26192  elply2  26310  plypf1  26326  ulmcaulem  26511  ulmcau  26512  ulmss  26514  ulmdvlem3  26519  mtest  26521  itgulm  26525  abelthlem8  26556  abelth  26558  tanord  26657  cxpcn3lem  26866  mcubic  26966  cubic2  26967  dvdsflsumcom  27306  fsumdvdsmul  27313  lgsdchrval  27472  2sqlem9  27545  rplogsumlem2  27603  rpvmasumlem  27605  dchrvmasumlem1  27613  vmalogdivsum2  27656  logsqvma  27660  selberg  27666  selberg4  27679  pntibndlem3  27710  pntlem3  27727  pntleml  27729  padicabv  27748  padicabvf  27749  padicabvcxp  27750  ostth3  27756  nosupbnd1lem5  27830  noinfbnd1lem5  27845  nocvxminlem  27901  lrrecfr  28090  addsprop  28123  mulsproplem9  28271  mulsproplem12  28274  mulsproplem13  28275  mulsproplem14  28276  mulsprop  28277  lemulsd  28285  mulsuniflem  28296  mulsasslem3  28312  axpasch  29196  axcontlem7  29225  axcontlem10  29228  cusgrsize2inds  29708  grpolcan  30787  nvmul0or  30907  nmosetre  31021  blocnilem  31061  blocni  31062  h2hcau  31236  h2hlm  31237  shsel3  31572  chscllem2  31895  homulcl  32016  adjsym  32090  cnvadj  32149  hhcno  32161  hhcnf  32162  lnopl  32171  unoplin  32177  counop  32178  lnfnl  32188  hmoplin  32199  hmopm  32278  nmcexi  32283  lnconi  32290  riesz3i  32319  leopmuli  32390  leopmul  32391  hstle  32487  mdsl0  32567  mdslmd1lem2  32583  atcvatlem  32642  chirredi  32651  cdj1i  32690  sbc2iedf  32718  foresf1o  32756  suppovss  32934  isoun  32955  difioo  33035  swrdf1  33184  xrge0tsmsd  33301  cycpmrn  33371  ressply1invg  33771  ply1unit  33777  fedgmullem2  33932  pstmxmet  34199  ordtrest2NEWlem  34224  esum2dlem  34394  esum2d  34395  dya2icoseg2  34580  eulerpartlemgc  34664  eulerpartlemgh  34680  eulerpartlemgs2  34682  ballotlemimin  34808  signstfvneq0  34871  hgt750lemb  34955  connpconn  35593  cvmliftmolem2  35640  cvmliftlem6  35648  cvmliftlem8  35650  cvmlift2lem12  35672  elmrsubrn  35878  dfon2lem6  36144  ifscgr  36402  brsegle  36466  neibastop2lem  36728  bj-elabd2ALT  37417  bj-ismooredr2  37607  curf  38104  finixpnum  38111  fin2solem  38112  fin2so  38113  lindsenlbs  38121  matunitlindflem1  38122  matunitlindflem2  38123  matunitlindf  38124  poimirlem3  38129  poimirlem4  38130  poimirlem6  38132  poimirlem7  38133  poimirlem14  38140  poimirlem16  38142  poimirlem19  38145  poimirlem22  38148  poimirlem28  38154  poimirlem29  38155  poimirlem30  38156  poimir  38159  heicant  38161  itg2gt0cn  38181  ftc1cnnc  38198  ftc1anclem5  38203  ftc1anclem6  38204  ftc1anclem7  38205  ftc1anc  38207  cover2  38221  filbcmb  38246  fdc  38251  fdc1  38252  seqpo  38253  incsequz  38254  incsequz2  38255  metf1o  38261  lmclim2  38264  geomcau  38265  isbnd2  38289  bndss  38292  ismtybndlem  38312  heibor1lem  38315  rrncmslem  38338  rrnequiv  38341  exidreslem  38383  ghomco  38397  isdrngo3  38465  rngoisocnv  38487  isidlc  38521  idlnegcl  38528  divrngidl  38534  intidl  38535  unichnidl  38537  keridl  38538  igenmin  38570  prnc  38573  ispridlc  38576  erimeq2  39269  prter3  39513  glbconxN  40009  atltcvr  40066  3dim1  40098  lvolnle3at  40213  linepsubN  40383  osumclN  40598  pexmidALTN  40609  lhpmatb  40662  cdlemg1idlemN  41203  dihlss  41881  dihglblem5aN  41923  dihatlat  41965  aks6d1c1p1  42731  aks6d1c5lem1  42760  unitscyglem4  42822  fsuppind  43179  fsuppssindlem1  43180  prjspertr  43194  prjspreln0  43198  lsmfgcl  43658  kercvrlsm  43667  unxpwdom3  43679  hbt  43714  oa0suclim  43859  om0suclim  43860  oe0suclim  43861  naddcnff  43946  cvgdvgrat  44882  climinf  46181  clim2f  46209  clim2cf  46223  clim0cf  46227  clim2f2  46243  fmtnofac2lem  48176  ovmpordxf  48971  oppcthinendcALT  50071  cotsqcscsq  50392  aacllem  50431