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  3030  ralimdvva  3206  reximdvva  3207  2ralbidva  3219  2rexbidva  3220  2ralbida  3283  spcimgft  3546  copsexgw  5495  copsexg  5496  pofun  5610  imainss  6174  fvmptdf  7022  eqfnfv2  7052  fnex  7237  f1elima  7283  fliftfun  7332  isores2  7353  f1oiso  7371  ovmpodxf  7583  sorpssuni  7752  sorpssint  7753  tfindsg2  7883  2ndconst  8126  poxp2  8168  sexp3  8178  poseq  8183  oalim  8570  omlim  8571  oaass  8599  omlimcl  8616  omass  8618  oelim2  8633  oeoa  8635  oeoelem  8636  nnaass  8660  omabs  8689  eroveu  8852  sbthlem4  9126  fimaxg  9323  fisupg  9324  fofinf1o  9372  fiming  9538  fiinfg  9539  ordtypelem7  9564  hartogs  9584  card2on  9594  unwdomg  9624  wemapwe  9737  frmin  9789  dfac5  10169  cfsmolem  10310  isf32lem2  10394  ttukeylem6  10554  ondomon  10603  alephreg  10622  ltexprlem6  11081  recexsrlem  11143  wloglei  11795  recextlem2  11894  fimaxre  12212  creur  12260  uz11  12903  xrmaxeq  13221  xrmineq  13222  xaddf  13266  xaddass  13291  xleadd1a  13295  xlt2add  13302  xmullem  13306  xmulgt0  13325  xmulasslem3  13328  xlemul1a  13330  xadddilem  13336  fzrevral  13652  seqcaopr2  14079  expnlbnd2  14273  faclbnd4lem4  14335  hashgt23el  14463  rtrclreclem3  15099  rtrclreclem4  15100  relexpindlem  15102  rtrclind  15104  shftlem  15107  01sqrex  15288  cau3lem  15393  limsupbnd2  15519  clim2  15540  clim2c  15541  clim0c  15543  rlimresb  15601  2clim  15608  climabs0  15621  climcn1  15628  climcn2  15629  o1rlimmul  15655  climsqz  15677  climsqz2  15678  rlimsqzlem  15685  lo1le  15688  climsup  15706  caucvgrlem2  15711  iseralt  15721  summolem2  15752  fsum2dlem  15806  cvgcmp  15852  cvgcmpce  15854  climfsum  15856  fsumiun  15857  geomulcvg  15912  mertenslem2  15921  mertens  15922  prodfn0  15930  prodfrec  15931  zprod  15973  fprodeq0  16011  fprodn0  16015  fprod2dlem  16016  smu01lem  16522  gcdcllem1  16536  dvdssq  16604  lcmdvds  16645  coprmdvds2  16691  pclem  16876  pcge0  16900  pcgcd1  16915  prmpwdvds  16942  1arithlem4  16964  4sqlem18  17000  vdwlem10  17028  vdwlem11  17029  ramval  17046  ramub1lem2  17065  ramcl  17067  imasaddfnlem  17573  imasaddflem  17575  imasvscafn  17582  imasleval  17586  ismon2  17778  isepi2  17785  issubc3  17894  cofucl  17933  setcmon  18132  setcepi  18133  ipodrsfi  18584  ipodrsima  18586  isacs3lem  18587  grpidpropd  18675  grprida  18688  gsumpropd2lem  18692  mgmhmpropd  18711  mgmhmima  18728  mhmpropd  18805  mhmimalem  18837  grplcan  19018  dfgrp3lem  19056  mulgdirlem  19123  subgmulg  19158  issubg4  19163  subgint  19168  ssnmz  19184  cycsubgcl  19224  gastacl  19327  orbsta  19331  cntzsubg  19357  galactghm  19422  odmulg  19574  odbezout  19576  sylow3lem2  19646  lsmsubm  19671  efgsfo  19757  mulgmhm  19845  mulgghm  19846  gsumval3  19925  gsumcllem  19926  gsumpt  19980  gsum2d  19990  gsum2d2  19992  prdsgsum  19999  subgdmdprd  20054  dprd2d2  20064  ablfac1eu  20093  rngpropd  20171  srglmhm  20218  srgrmhm  20219  ringpropd  20285  ringlghm  20309  dvdsrpropd  20416  rhmimasubrnglem  20565  cntzsdrg  20803  abvpropd  20836  islmodd  20864  lmodprop2d  20922  lsssubg  20955  lsspropd  21016  lmhmima  21046  lidlsubg  21233  phlpropd  21673  frlmsslsp  21816  lindfmm  21847  islindf4  21858  assapropd  21892  asclpropd  21917  psrass1lem  21952  mplcoe1  22055  mplcoe5  22058  mplind  22094  evlslem2  22103  evlsval  22110  coe1tmmul2  22279  mamuass  22406  mavmulass  22555  mdetuni0  22627  mdetmul  22629  cpmatacl  22722  cpmadugsumfi  22883  cpmadumatpolylem1  22887  cpmadumatpolylem2  22888  cpmadumatpoly  22889  cayhamlem4  22894  neips  23121  neindisj  23125  ordtrest2lem  23211  lmbrf  23268  lmss  23306  isreg2  23385  lmmo  23388  hauscmplem  23414  bwth  23418  2ndcomap  23466  1stcelcls  23469  restlly  23491  islly2  23492  cldllycmp  23503  comppfsc  23540  1stckgenlem  23561  txbas  23575  txbasval  23614  tx1cn  23617  ptpjopn  23620  ptcnp  23630  txnlly  23645  txlm  23656  xkococn  23668  fgabs  23887  fmfnfmlem4  23965  flimcf  23990  hauspwpwf1  23995  fclsbas  24029  fclscf  24033  flimfnfcls  24036  ghmcnp  24123  tsmsxp  24163  isxmet2d  24337  elmopn2  24455  mopni3  24507  blsscls2  24517  metequiv2  24523  metss2lem  24524  met2ndci  24535  metrest  24537  metcnp  24554  metcnp2  24555  metcnpi3  24559  txmetcnp  24560  nmolb2d  24739  xrge0tsms  24856  metdsre  24875  metnrmlem3  24883  fsumcn  24894  elcncf2  24916  mulc1cncf  24931  cncfco  24933  cncfmet  24935  bndth  24990  evth  24991  copco  25051  pcopt2  25056  pcoass  25057  pcorevlem  25059  lmmcvg  25295  lmmbrf  25296  iscau4  25313  iscauf  25314  cmetcaulem  25322  iscmet3lem3  25324  iscmet3lem1  25325  causs  25332  equivcfil  25333  lmclim  25337  caubl  25342  caublcls  25343  bcth3  25365  ivthle  25491  ivthle2  25492  ovoliunlem1  25537  ovolicc2lem5  25556  volsuplem  25590  uniioombllem6  25623  dyaddisjlem  25630  dyadmax  25633  volcn  25641  mbfmulc2lem  25682  ismbf3d  25689  mbfsup  25699  mbfinf  25700  mbflim  25703  i1fmullem  25729  itg2seq  25777  itg2uba  25778  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  bddiblnc  25877  ditgsplitlem  25895  ellimc2  25912  ellimc3  25914  limcflf  25916  limcmpt  25918  limcco  25928  lhop1lem  26052  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumrlim  26072  ftc1a  26078  ftc1lem6  26082  mdegmullem  26117  elply2  26235  plypf1  26251  ulmcaulem  26437  ulmcau  26438  ulmss  26440  ulmdvlem3  26445  mtest  26447  itgulm  26451  abelthlem8  26483  abelth  26485  tanord  26580  cxpcn3lem  26790  mcubic  26890  cubic2  26891  dvdsflsumcom  27231  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  lgsdchrval  27398  2sqlem9  27471  rplogsumlem2  27529  rpvmasumlem  27531  dchrvmasumlem1  27539  vmalogdivsum2  27582  logsqvma  27586  selberg  27592  selberg4  27605  pntibndlem3  27636  pntlem3  27653  pntleml  27655  padicabv  27674  padicabvf  27675  padicabvcxp  27676  ostth3  27682  nosupbnd1lem5  27757  noinfbnd1lem5  27772  nocvxminlem  27822  lrrecfr  27976  addsprop  28009  mulsproplem9  28150  mulsproplem12  28153  mulsproplem13  28154  mulsproplem14  28155  mulsprop  28156  slemuld  28164  mulsuniflem  28175  mulsasslem3  28191  axpasch  28956  axcontlem7  28985  axcontlem10  28988  cusgrsize2inds  29471  grpolcan  30549  nvmul0or  30669  nmosetre  30783  blocnilem  30823  blocni  30824  h2hcau  30998  h2hlm  30999  shsel3  31334  chscllem2  31657  homulcl  31778  adjsym  31852  cnvadj  31911  hhcno  31923  hhcnf  31924  lnopl  31933  unoplin  31939  counop  31940  lnfnl  31950  hmoplin  31961  hmopm  32040  nmcexi  32045  lnconi  32052  riesz3i  32081  leopmuli  32152  leopmul  32153  hstle  32249  mdsl0  32329  mdslmd1lem2  32345  atcvatlem  32404  chirredi  32413  cdj1i  32452  sbc2iedf  32484  foresf1o  32523  suppovss  32690  isoun  32711  difioo  32784  swrdf1  32941  xrge0tsmsd  33065  cycpmrn  33163  ressply1invg  33594  ply1unit  33600  fedgmullem2  33681  pstmxmet  33896  ordtrest2NEWlem  33921  esum2dlem  34093  esum2d  34094  dya2icoseg2  34280  eulerpartlemgc  34364  eulerpartlemgh  34380  eulerpartlemgs2  34382  ballotlemimin  34508  signstfvneq0  34587  hgt750lemb  34671  connpconn  35240  cvmliftmolem2  35287  cvmliftlem6  35295  cvmliftlem8  35297  cvmlift2lem12  35319  elmrsubrn  35525  dfon2lem6  35789  ifscgr  36045  brsegle  36109  neibastop2lem  36361  bj-elabd2ALT  36926  bj-ismooredr2  37111  curf  37605  finixpnum  37612  fin2solem  37613  fin2so  37614  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  matunitlindf  37625  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem14  37641  poimirlem16  37643  poimirlem19  37646  poimirlem22  37649  poimirlem28  37655  poimirlem29  37656  poimirlem30  37657  poimir  37660  heicant  37662  itg2gt0cn  37682  ftc1cnnc  37699  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anc  37708  cover2  37722  filbcmb  37747  fdc  37752  fdc1  37753  seqpo  37754  incsequz  37755  incsequz2  37756  metf1o  37762  lmclim2  37765  geomcau  37766  isbnd2  37790  bndss  37793  ismtybndlem  37813  heibor1lem  37816  rrncmslem  37839  rrnequiv  37842  exidreslem  37884  ghomco  37898  isdrngo3  37966  rngoisocnv  37988  isidlc  38022  idlnegcl  38029  divrngidl  38035  intidl  38036  unichnidl  38038  keridl  38039  igenmin  38071  prnc  38074  ispridlc  38077  erimeq2  38679  prter3  38883  glbconxN  39380  atltcvr  39437  3dim1  39469  lvolnle3at  39584  linepsubN  39754  osumclN  39969  pexmidALTN  39980  lhpmatb  40033  cdlemg1idlemN  40574  dihlss  41252  dihglblem5aN  41294  dihatlat  41336  aks6d1c1p1  42108  aks6d1c5lem1  42137  unitscyglem4  42199  metakunt1  42206  metakunt2  42207  f1o2d2  42274  pwsgprod  42554  selvvvval  42595  fsuppind  42600  fsuppssindlem1  42601  prjspertr  42615  prjspreln0  42619  lsmfgcl  43086  kercvrlsm  43095  unxpwdom3  43107  hbt  43142  oa0suclim  43288  om0suclim  43289  oe0suclim  43290  naddcnff  43375  cvgdvgrat  44332  climinf  45621  clim2f  45651  clim2cf  45665  clim0cf  45669  clim2f2  45685  fmtnofac2lem  47555  ovmpordxf  48255  oppcthinendcALT  49090  cotsqcscsq  49281  aacllem  49320