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  652  anabss5  665  anabss7  670  mpanr1  700  pm2.61ddan  811  pm2.61dda  812  pm2.61da2ne  3022  ralimdvva  3196  reximdvva  3197  2ralbidva  3208  2rexbidva  3209  2ralbida  3272  copsexgw  5480  copsexg  5481  pofun  5596  imainss  6143  fvmptdf  6994  eqfnfv2  7023  fnex  7210  f1elima  7254  fliftfun  7301  isores2  7322  f1oiso  7340  ovmpodxf  7550  sorpssuni  7715  sorpssint  7716  tfindsg2  7844  2ndconst  8081  poxp2  8123  sexp3  8133  poseq  8138  oalim  8527  omlim  8528  oaass  8556  omlimcl  8573  omass  8575  oelim2  8590  oeoa  8592  oeoelem  8593  nnaass  8617  omabs  8646  eroveu  8802  sbthlem4  9082  fimaxg  9286  fisupg  9287  fofinf1o  9323  fiming  9489  fiinfg  9490  ordtypelem7  9515  hartogs  9535  card2on  9545  unwdomg  9575  wemapwe  9688  frmin  9740  dfac5  10119  cfsmolem  10261  isf32lem2  10345  ttukeylem6  10505  ondomon  10554  alephreg  10573  ltexprlem6  11032  recexsrlem  11094  wloglei  11743  recextlem2  11842  fimaxre  12155  creur  12203  uz11  12844  xrmaxeq  13155  xrmineq  13156  xaddf  13200  xaddass  13225  xleadd1a  13229  xlt2add  13236  xmullem  13240  xmulgt0  13259  xmulasslem3  13262  xlemul1a  13264  xadddilem  13270  fzrevral  13583  seqcaopr2  14001  expnlbnd2  14194  faclbnd4lem4  14253  hashgt23el  14381  rtrclreclem3  15004  rtrclreclem4  15005  relexpindlem  15007  rtrclind  15009  shftlem  15012  01sqrex  15193  cau3lem  15298  limsupbnd2  15424  clim2  15445  clim2c  15446  clim0c  15448  rlimresb  15506  2clim  15513  climabs0  15526  climcn1  15533  climcn2  15534  o1rlimmul  15560  climsqz  15582  climsqz2  15583  rlimsqzlem  15592  lo1le  15595  climsup  15613  caucvgrlem2  15618  iseralt  15628  summolem2  15659  fsum2dlem  15713  cvgcmp  15759  cvgcmpce  15761  climfsum  15763  fsumiun  15764  geomulcvg  15819  mertenslem2  15828  mertens  15829  prodfn0  15837  prodfrec  15838  zprod  15878  fprodeq0  15916  fprodn0  15920  fprod2dlem  15921  smu01lem  16423  gcdcllem1  16437  dvdssq  16501  lcmdvds  16542  coprmdvds2  16588  pclem  16770  pcge0  16794  pcgcd1  16809  prmpwdvds  16836  1arithlem4  16858  4sqlem18  16894  vdwlem10  16922  vdwlem11  16923  ramval  16940  ramub1lem2  16959  ramcl  16961  imasaddfnlem  17473  imasaddflem  17475  imasvscafn  17482  imasleval  17486  ismon2  17680  isepi2  17687  issubc3  17798  cofucl  17837  setcmon  18039  setcepi  18040  ipodrsfi  18494  ipodrsima  18496  isacs3lem  18497  grpidpropd  18585  grprida  18598  gsumpropd2lem  18602  mgmhmpropd  18621  mgmhmima  18638  mhmpropd  18712  mhmimalem  18739  grplcan  18920  dfgrp3lem  18956  mulgdirlem  19022  subgmulg  19057  issubg4  19062  subgint  19067  ssnmz  19083  cycsubgcl  19122  gastacl  19215  orbsta  19219  cntzsubg  19245  galactghm  19314  odmulg  19466  odbezout  19468  sylow3lem2  19538  lsmsubm  19563  efgsfo  19649  mulgmhm  19737  mulgghm  19738  gsumval3  19817  gsumcllem  19818  gsumpt  19872  gsum2d  19882  gsum2d2  19884  prdsgsum  19891  subgdmdprd  19946  dprd2d2  19956  ablfac1eu  19985  rngpropd  20069  srglmhm  20116  srgrmhm  20117  ringpropd  20177  ringlghm  20201  dvdsrpropd  20308  rhmimasubrnglem  20455  cntzsdrg  20643  abvpropd  20675  islmodd  20702  lmodprop2d  20760  lsssubg  20794  lsspropd  20855  lmhmima  20885  lidlsubg  21072  phlpropd  21516  frlmsslsp  21659  lindfmm  21690  islindf4  21701  assapropd  21734  asclpropd  21759  psrass1lemOLD  21802  psrass1lem  21805  mplcoe1  21902  mplcoe5  21905  mplind  21941  evlslem2  21952  evlsval  21959  coe1tmmul2  22117  mamuass  22224  mavmulass  22373  mdetuni0  22445  mdetmul  22447  cpmatacl  22540  cpmadugsumfi  22701  cpmadumatpolylem1  22705  cpmadumatpolylem2  22706  cpmadumatpoly  22707  cayhamlem4  22712  neips  22939  neindisj  22943  ordtrest2lem  23029  lmbrf  23086  lmss  23124  isreg2  23203  lmmo  23206  hauscmplem  23232  bwth  23236  2ndcomap  23284  1stcelcls  23287  restlly  23309  islly2  23310  cldllycmp  23321  comppfsc  23358  1stckgenlem  23379  txbas  23393  txbasval  23432  tx1cn  23435  ptpjopn  23438  ptcnp  23448  txnlly  23463  txlm  23474  xkococn  23486  fgabs  23705  fmfnfmlem4  23783  flimcf  23808  hauspwpwf1  23813  fclsbas  23847  fclscf  23851  flimfnfcls  23854  ghmcnp  23941  tsmsxp  23981  isxmet2d  24155  elmopn2  24273  mopni3  24325  blsscls2  24335  metequiv2  24341  metss2lem  24342  met2ndci  24353  metrest  24355  metcnp  24372  metcnp2  24373  metcnpi3  24377  txmetcnp  24378  nmolb2d  24557  xrge0tsms  24672  metdsre  24691  metnrmlem3  24699  fsumcn  24710  elcncf2  24732  mulc1cncf  24747  cncfco  24749  cncfmet  24751  bndth  24806  evth  24807  copco  24867  pcopt2  24872  pcoass  24873  pcorevlem  24875  lmmcvg  25111  lmmbrf  25112  iscau4  25129  iscauf  25130  cmetcaulem  25138  iscmet3lem3  25140  iscmet3lem1  25141  causs  25148  equivcfil  25149  lmclim  25153  caubl  25158  caublcls  25159  bcth3  25181  ivthle  25307  ivthle2  25308  ovoliunlem1  25353  ovolicc2lem5  25372  volsuplem  25406  uniioombllem6  25439  dyaddisjlem  25446  dyadmax  25449  volcn  25457  mbfmulc2lem  25498  ismbf3d  25505  mbfsup  25515  mbfinf  25516  mbflim  25519  i1fmullem  25545  itg2seq  25594  itg2uba  25595  itg2splitlem  25600  itg2split  25601  itg2monolem1  25602  bddiblnc  25693  ditgsplitlem  25711  ellimc2  25728  ellimc3  25730  limcflf  25732  limcmpt  25734  limcco  25744  lhop1lem  25868  dvfsumle  25876  dvfsumleOLD  25877  dvfsumabs  25879  dvfsumrlim  25888  ftc1a  25894  ftc1lem6  25898  mdegmullem  25936  elply2  26050  plypf1  26066  ulmcaulem  26247  ulmcau  26248  ulmss  26250  ulmdvlem3  26255  mtest  26257  itgulm  26261  abelthlem8  26293  abelth  26295  tanord  26389  cxpcn3lem  26598  mcubic  26695  cubic2  26696  dvdsflsumcom  27036  fsumdvdsmul  27043  fsumdvdsmulOLD  27045  lgsdchrval  27203  2sqlem9  27276  rplogsumlem2  27334  rpvmasumlem  27336  dchrvmasumlem1  27344  vmalogdivsum2  27387  logsqvma  27391  selberg  27397  selberg4  27410  pntibndlem3  27441  pntlem3  27458  pntleml  27460  padicabv  27479  padicabvf  27480  padicabvcxp  27481  ostth3  27487  nosupbnd1lem5  27561  noinfbnd1lem5  27576  nocvxminlem  27626  lrrecfr  27776  addsprop  27809  mulsproplem9  27940  mulsproplem12  27943  mulsproplem13  27944  mulsproplem14  27945  mulsprop  27946  slemuld  27954  mulsuniflem  27965  mulsasslem3  27981  axpasch  28668  axcontlem7  28697  axcontlem10  28700  cusgrsize2inds  29179  grpolcan  30252  nvmul0or  30372  nmosetre  30486  blocnilem  30526  blocni  30527  h2hcau  30701  h2hlm  30702  shsel3  31037  chscllem2  31360  homulcl  31481  adjsym  31555  cnvadj  31614  hhcno  31626  hhcnf  31627  lnopl  31636  unoplin  31642  counop  31643  lnfnl  31653  hmoplin  31664  hmopm  31743  nmcexi  31748  lnconi  31755  riesz3i  31784  leopmuli  31855  leopmul  31856  hstle  31952  mdsl0  32032  mdslmd1lem2  32048  atcvatlem  32107  chirredi  32116  cdj1i  32155  sbc2iedf  32176  foresf1o  32211  suppovss  32375  isoun  32392  difioo  32462  swrdf1  32587  xrge0tsmsd  32677  cycpmrn  32770  ressply1invg  33125  fedgmullem2  33194  pstmxmet  33366  ordtrest2NEWlem  33391  esum2dlem  33579  esum2d  33580  dya2icoseg2  33766  eulerpartlemgc  33850  eulerpartlemgh  33866  eulerpartlemgs2  33868  ballotlemimin  33993  signstfvneq0  34072  hgt750lemb  34157  connpconn  34715  cvmliftmolem2  34762  cvmliftlem6  34770  cvmliftlem8  34772  cvmlift2lem12  34794  elmrsubrn  35000  dfon2lem6  35255  ifscgr  35511  brsegle  35575  neibastop2lem  35735  bj-elabd2ALT  36295  bj-ismooredr2  36481  curf  36956  finixpnum  36963  fin2solem  36964  fin2so  36965  lindsenlbs  36973  matunitlindflem1  36974  matunitlindflem2  36975  matunitlindf  36976  poimirlem3  36981  poimirlem4  36982  poimirlem6  36984  poimirlem7  36985  poimirlem14  36992  poimirlem16  36994  poimirlem19  36997  poimirlem22  37000  poimirlem28  37006  poimirlem29  37007  poimirlem30  37008  poimir  37011  heicant  37013  itg2gt0cn  37033  ftc1cnnc  37050  ftc1anclem5  37055  ftc1anclem6  37056  ftc1anclem7  37057  ftc1anc  37059  cover2  37073  filbcmb  37098  fdc  37103  fdc1  37104  seqpo  37105  incsequz  37106  incsequz2  37107  metf1o  37113  lmclim2  37116  geomcau  37117  isbnd2  37141  bndss  37144  ismtybndlem  37164  heibor1lem  37167  rrncmslem  37190  rrnequiv  37193  exidreslem  37235  ghomco  37249  isdrngo3  37317  rngoisocnv  37339  isidlc  37373  idlnegcl  37380  divrngidl  37386  intidl  37387  unichnidl  37389  keridl  37390  igenmin  37422  prnc  37425  ispridlc  37428  erimeq2  38038  prter3  38242  glbconxN  38739  atltcvr  38796  3dim1  38828  lvolnle3at  38943  linepsubN  39113  osumclN  39328  pexmidALTN  39339  lhpmatb  39392  cdlemg1idlemN  39933  dihlss  40611  dihglblem5aN  40653  dihatlat  40695  metakunt1  41478  metakunt2  41479  f1o2d2  41548  pwsgprod  41603  selvvvval  41646  fsuppind  41651  fsuppssindlem1  41652  prjspertr  41836  prjspreln0  41840  lsmfgcl  42305  kercvrlsm  42314  unxpwdom3  42326  hbt  42361  oa0suclim  42514  om0suclim  42515  oe0suclim  42516  naddcnff  42601  cvgdvgrat  43561  climinf  44807  clim2f  44837  clim2cf  44851  clim0cf  44855  clim2f2  44871  fmtnofac2lem  46721  isomuspgrlem2d  46984  ovmpordxf  47203  cotsqcscsq  47995  aacllem  48036