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 206  df-an 396

This theorem is referenced by:  anass  468  anass1rs  651  anabss5  664  anabss7  669  mpanr1  699  pm2.61ddan  810  pm2.61dda  811  pm2.61da2ne  3032  ralimdvva  3104  2ralbidva  3121  2ralbida  3159  reximdvva  3205  2rexbidva  3227  copsexgw  5398  copsexg  5399  pofun  5512  imainss  6046  fvmptdf  6863  eqfnfv2  6892  fnex  7075  f1elima  7117  fliftfun  7163  isores2  7184  f1oiso  7202  ovmpodxf  7401  sorpssuni  7563  sorpssint  7564  tfindsg2  7683  2ndconst  7912  oalim  8324  omlim  8325  oaass  8354  omlimcl  8371  omass  8373  oelim2  8388  oeoa  8390  oeoelem  8391  nnaass  8415  omabs  8441  eroveu  8559  sbthlem4  8826  fimaxg  8991  fisupg  8992  fofinf1o  9024  fiming  9187  fiinfg  9188  ordtypelem7  9213  hartogs  9233  card2on  9243  unwdomg  9273  wemapwe  9385  dfac5  9815  cfsmolem  9957  isf32lem2  10041  ttukeylem6  10201  ondomon  10250  alephreg  10269  ltexprlem6  10728  recexsrlem  10790  wloglei  11437  recextlem2  11536  fimaxre  11849  creur  11897  uz11  12536  xrmaxeq  12842  xrmineq  12843  xaddf  12887  xaddass  12912  xleadd1a  12916  xlt2add  12923  xmullem  12927  xmulgt0  12946  xmulasslem3  12949  xlemul1a  12951  xadddilem  12957  fzrevral  13270  seqcaopr2  13687  expnlbnd2  13877  faclbnd4lem4  13938  hashgt23el  14067  rtrclreclem3  14699  rtrclreclem4  14700  relexpindlem  14702  rtrclind  14704  shftlem  14707  01sqrex  14889  cau3lem  14994  limsupbnd2  15120  clim2  15141  clim2c  15142  clim0c  15144  rlimresb  15202  2clim  15209  climabs0  15222  climcn1  15229  climcn2  15230  o1rlimmul  15256  climsqz  15278  climsqz2  15279  rlimsqzlem  15288  lo1le  15291  climsup  15309  caucvgrlem2  15314  iseralt  15324  summolem2  15356  fsum2dlem  15410  cvgcmp  15456  cvgcmpce  15458  climfsum  15460  fsumiun  15461  geomulcvg  15516  mertenslem2  15525  mertens  15526  prodfn0  15534  prodfrec  15535  zprod  15575  fprodeq0  15613  fprodn0  15617  fprod2dlem  15618  smu01lem  16120  gcdcllem1  16134  gcdmultiplezOLD  16189  dvdssq  16200  lcmdvds  16241  coprmdvds2  16287  pclem  16467  pcge0  16491  pcgcd1  16506  prmpwdvds  16533  1arithlem4  16555  4sqlem18  16591  vdwlem10  16619  vdwlem11  16620  ramval  16637  ramub1lem2  16656  ramcl  16658  imasaddfnlem  17156  imasaddflem  17158  imasvscafn  17165  imasleval  17169  ismon2  17363  isepi2  17370  issubc3  17480  cofucl  17519  setcmon  17718  setcepi  17719  ipodrsfi  18172  ipodrsima  18174  isacs3lem  18175  grpidpropd  18261  grpridd  18274  gsumpropd2lem  18278  mhmpropd  18351  mhmima  18378  gsumccatOLD  18394  grplcan  18552  dfgrp3lem  18588  mulgdirlem  18649  subgmulg  18684  issubg4  18689  subgint  18694  ssnmz  18709  cycsubgcl  18740  gastacl  18830  orbsta  18834  cntzsubg  18858  galactghm  18927  odmulg  19078  odbezout  19080  sylow3lem2  19148  lsmsubm  19173  efgsfo  19260  mulgmhm  19344  mulgghm  19345  gsumval3  19423  gsumcllem  19424  gsumpt  19478  gsum2d  19488  gsum2d2  19490  prdsgsum  19497  subgdmdprd  19552  dprd2d2  19562  ablfac1eu  19591  srglmhm  19686  srgrmhm  19687  ringpropd  19736  ringlghm  19758  dvdsrpropd  19853  cntzsdrg  19985  abvpropd  20017  islmodd  20044  lmodprop2d  20100  lsssubg  20134  lsspropd  20194  lmhmima  20224  lidlsubg  20399  phlpropd  20772  frlmsslsp  20913  lindfmm  20944  islindf4  20955  assapropd  20986  asclpropd  21011  psrass1lemOLD  21053  psrass1lem  21056  mplcoe1  21148  mplcoe5  21151  mplind  21188  evlslem2  21199  evlsval  21206  coe1tmmul2  21357  mamuass  21459  mavmulass  21606  mdetuni0  21678  mdetmul  21680  cpmatacl  21773  cpmadugsumfi  21934  cpmadumatpolylem1  21938  cpmadumatpolylem2  21939  cpmadumatpoly  21940  cayhamlem4  21945  neips  22172  neindisj  22176  ordtrest2lem  22262  lmbrf  22319  lmss  22357  isreg2  22436  lmmo  22439  hauscmplem  22465  bwth  22469  2ndcomap  22517  1stcelcls  22520  restlly  22542  islly2  22543  cldllycmp  22554  comppfsc  22591  1stckgenlem  22612  txbas  22626  txbasval  22665  tx1cn  22668  ptpjopn  22671  ptcnp  22681  txnlly  22696  txlm  22707  xkococn  22719  fgabs  22938  fmfnfmlem4  23016  flimcf  23041  hauspwpwf1  23046  fclsbas  23080  fclscf  23084  flimfnfcls  23087  ghmcnp  23174  tsmsxp  23214  isxmet2d  23388  elmopn2  23506  mopni3  23556  blsscls2  23566  metequiv2  23572  metss2lem  23573  met2ndci  23584  metrest  23586  metcnp  23603  metcnp2  23604  metcnpi3  23608  txmetcnp  23609  nmolb2d  23788  xrge0tsms  23903  metdsre  23922  metnrmlem3  23930  fsumcn  23939  elcncf2  23959  mulc1cncf  23974  cncfco  23976  cncfmet  23978  bndth  24027  evth  24028  copco  24087  pcopt2  24092  pcoass  24093  pcorevlem  24095  lmmcvg  24330  lmmbrf  24331  iscau4  24348  iscauf  24349  cmetcaulem  24357  iscmet3lem3  24359  iscmet3lem1  24360  causs  24367  equivcfil  24368  lmclim  24372  caubl  24377  caublcls  24378  bcth3  24400  ivthle  24525  ivthle2  24526  ovoliunlem1  24571  ovolicc2lem5  24590  volsuplem  24624  uniioombllem6  24657  dyaddisjlem  24664  dyadmax  24667  volcn  24675  mbfmulc2lem  24716  ismbf3d  24723  mbfsup  24733  mbfinf  24734  mbflim  24737  i1fmullem  24763  itg2seq  24812  itg2uba  24813  itg2splitlem  24818  itg2split  24819  itg2monolem1  24820  bddiblnc  24911  ditgsplitlem  24929  ellimc2  24946  ellimc3  24948  limcflf  24950  limcmpt  24952  limcco  24962  lhop1lem  25082  dvfsumle  25090  dvfsumabs  25092  dvfsumrlim  25100  ftc1a  25106  ftc1lem6  25110  mdegmullem  25148  elply2  25262  plypf1  25278  ulmcaulem  25458  ulmcau  25459  ulmss  25461  ulmdvlem3  25466  mtest  25468  itgulm  25472  abelthlem8  25503  abelth  25505  tanord  25599  cxpcn3lem  25805  mcubic  25902  cubic2  25903  dvdsflsumcom  26242  fsumdvdsmul  26249  lgsdchrval  26407  2sqlem9  26480  rplogsumlem2  26538  rpvmasumlem  26540  dchrvmasumlem1  26548  vmalogdivsum2  26591  logsqvma  26595  selberg  26601  selberg4  26614  pntibndlem3  26645  pntlem3  26662  pntleml  26664  padicabv  26683  padicabvf  26684  padicabvcxp  26685  ostth3  26691  axpasch  27212  axcontlem7  27241  axcontlem10  27244  cusgrsize2inds  27723  grpolcan  28793  nvmul0or  28913  nmosetre  29027  blocnilem  29067  blocni  29068  h2hcau  29242  h2hlm  29243  shsel3  29578  chscllem2  29901  homulcl  30022  adjsym  30096  cnvadj  30155  hhcno  30167  hhcnf  30168  lnopl  30177  unoplin  30183  counop  30184  lnfnl  30194  hmoplin  30205  hmopm  30284  nmcexi  30289  lnconi  30296  riesz3i  30325  leopmuli  30396  leopmul  30397  hstle  30493  mdsl0  30573  mdslmd1lem2  30589  atcvatlem  30648  chirredi  30657  cdj1i  30696  sbc2iedf  30716  foresf1o  30751  suppovss  30919  isoun  30936  difioo  31005  swrdf1  31130  xrge0tsmsd  31219  cycpmrn  31312  fedgmullem2  31613  pstmxmet  31749  ordtrest2NEWlem  31774  esum2dlem  31960  esum2d  31961  dya2icoseg2  32145  eulerpartlemgc  32229  eulerpartlemgh  32245  eulerpartlemgs2  32247  ballotlemimin  32372  signstfvneq0  32451  hgt750lemb  32536  connpconn  33097  cvmliftmolem2  33144  cvmliftlem6  33152  cvmliftlem8  33154  cvmlift2lem12  33176  elmrsubrn  33382  dfon2lem6  33670  poxp2  33717  xpord3pred  33725  sexp3  33726  poseq  33729  nosupbnd1lem5  33842  noinfbnd1lem5  33857  nocvxminlem  33899  lrrecfr  34027  ifscgr  34273  brsegle  34337  neibastop2lem  34476  bj-elabd2ALT  35040  bj-ismooredr2  35208  curf  35682  finixpnum  35689  fin2solem  35690  fin2so  35691  lindsenlbs  35699  matunitlindflem1  35700  matunitlindflem2  35701  matunitlindf  35702  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem14  35718  poimirlem16  35720  poimirlem19  35723  poimirlem22  35726  poimirlem28  35732  poimirlem29  35733  poimirlem30  35734  poimir  35737  heicant  35739  itg2gt0cn  35759  ftc1cnnc  35776  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anc  35785  cover2  35799  filbcmb  35825  fdc  35830  fdc1  35831  seqpo  35832  incsequz  35833  incsequz2  35834  metf1o  35840  lmclim2  35843  geomcau  35844  isbnd2  35868  bndss  35871  ismtybndlem  35891  heibor1lem  35894  rrncmslem  35917  rrnequiv  35920  exidreslem  35962  ghomco  35976  isdrngo3  36044  rngoisocnv  36066  isidlc  36100  idlnegcl  36107  divrngidl  36113  intidl  36114  unichnidl  36116  keridl  36117  igenmin  36149  prnc  36152  ispridlc  36155  erim2  36716  prter3  36823  glbconxN  37319  atltcvr  37376  3dim1  37408  lvolnle3at  37523  linepsubN  37693  osumclN  37908  pexmidALTN  37919  lhpmatb  37972  cdlemg1idlemN  38513  dihlss  39191  dihglblem5aN  39233  dihatlat  39275  metakunt1  40053  metakunt2  40054  pwsgprod  40194  fsuppind  40202  fsuppssindlem1  40203  prjspertr  40365  prjspreln0  40369  lsmfgcl  40815  kercvrlsm  40824  unxpwdom3  40836  hbt  40871  cvgdvgrat  41820  climinf  43037  clim2f  43067  clim2cf  43081  clim0cf  43085  clim2f2  43101  fmtnofac2lem  44908  isomuspgrlem2d  45171  mgmhmpropd  45227  mgmhmima  45244  ovmpordxf  45562  cotsqcscsq  46350  aacllem  46391