Theorem anassrs 471

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anass  472  anass1rs  665  anabss5  678  anabss7  683  mpanr1  713  pm2.61ddan  823  pm2.61dda  824  pm2.61da2ne  3044  ralimdvva  3208  reximdvva  3209  2ralbidva  3223  2rexbidva  3224  2ralbida  3284  spcimgft  3513  copsexgwOLD  5458  copsexg  5459  pofun  5571  imainss  6136  fvmptdf  6978  eqfnfv2  7008  fnex  7197  f1elima  7243  fliftfun  7292  isores2  7313  f1oiso  7331  ovmpodxf  7542  sorpssuni  7711  sorpssint  7712  tfindsg2  7838  2ndconst  8075  mpof1o2d  8100  poxp2  8118  sexp3  8128  poseq  8133  oalim  8496  omlim  8497  oaass  8525  omlimcl  8542  omass  8544  oelim2  8560  oeoa  8562  oeoelem  8563  nnaass  8587  omabs  8616  eroveu  8789  sbthlem4  9058  fimaxg  9227  fisupg  9228  fofinf1o  9272  fiming  9443  fiinfg  9444  ordtypelem7  9469  hartogs  9489  card2on  9499  unwdomg  9529  wemapwe  9649  frmin  9704  dfac5  10082  cfsmolem  10224  isf32lem2  10308  ttukeylem6  10468  ondomon  10517  alephreg  10537  ltexprlem6  10996  recexsrlem  11058  wloglei  11716  recextlem2  11815  fimaxre  12133  creur  12186  uz11  12861  xrmaxeq  13179  xrmineq  13180  xaddf  13224  xaddass  13249  xleadd1a  13253  xlt2add  13260  xmullem  13264  xmulgt0  13283  xmulasslem3  13286  xlemul1a  13288  xadddilem  13294  fzrevral  13614  seqcaopr2  14048  expnlbnd2  14244  faclbnd4lem4  14306  hashgt23el  14434  rtrclreclem3  15070  rtrclreclem4  15071  relexpindlem  15073  rtrclind  15075  shftlem  15078  01sqrex  15259  cau3lem  15365  limsupbnd2  15493  clim2  15514  clim2c  15515  clim0c  15517  rlimresb  15575  2clim  15582  climabs0  15595  climcn1  15602  climcn2  15603  o1rlimmul  15629  climsqz  15651  climsqz2  15652  rlimsqzlem  15659  lo1le  15662  climsup  15680  caucvgrlem2  15685  iseralt  15695  summolem2  15726  fsum2dlem  15780  cvgcmp  15827  cvgcmpce  15829  climfsum  15831  fsumiun  15832  geomulcvg  15889  mertenslem2  15898  mertens  15899  prodfn0  15907  prodfrec  15908  zprod  15950  fprodeq0  15988  fprodn0  15992  fprod2dlem  15993  smu01lem  16502  gcdcllem1  16516  dvdssq  16584  lcmdvds  16625  coprmdvds2  16671  pclem  16857  pcge0  16881  pcgcd1  16896  prmpwdvds  16923  1arithlem4  16945  4sqlem18  16981  vdwlem10  17009  vdwlem11  17010  ramval  17027  ramub1lem2  17046  ramcl  17048  imasaddfnlem  17541  imasaddflem  17543  imasvscafn  17550  imasleval  17554  ismon2  17750  isepi2  17757  issubc3  17865  cofucl  17904  setcmon  18103  setcepi  18104  ipodrsfi  18554  ipodrsima  18556  isacs3lem  18557  grpidpropd  18679  grprida  18692  gsumpropd2lem  18696  mgmhmpropd  18715  mgmhmima  18732  mhmpropd  18809  mhmimalem  18841  grplcan  19025  dfgrp3lem  19063  mulgdirlem  19130  subgmulg  19165  issubg4  19170  subgint  19175  ssnmz  19190  cycsubgcl  19230  gastacl  19332  orbsta  19336  cntzsubg  19362  galactghm  19427  odmulg  19579  odbezout  19581  sylow3lem2  19651  lsmsubm  19676  efgsfo  19762  mulgmhm  19850  mulgghm  19851  gsumval3  19930  gsumcllem  19931  gsumpt  19985  gsum2d  19995  gsum2d2  19997  prdsgsum  20004  subgdmdprd  20059  dprd2d2  20069  ablfac1eu  20098  rngpropd  20203  srglmhm  20250  srgrmhm  20251  ringpropd  20317  ringlghm  20341  pwsgprod  20357  dvdsrpropd  20444  rhmimasubrnglem  20594  cntzsdrg  20831  abvpropd  20864  islmodd  20913  lmodprop2d  20971  lsssubg  21004  lsspropd  21064  lmhmima  21094  lidlsubg  21273  phlpropd  21687  frlmsslsp  21828  lindfmm  21859  islindf4  21870  assapropd  21903  asclpropd  21929  psrass1lem  21965  mplcoe1  22070  mplcoe5  22073  mplind  22103  evlslem2  22112  evlsval  22119  selvvvval  22175  coe1tmmul2  22319  mamuass  22442  mavmulass  22589  mdetuni0  22661  mdetmul  22663  cpmatacl  22756  cpmadugsumfi  22917  cpmadumatpolylem1  22921  cpmadumatpolylem2  22922  cpmadumatpoly  22923  cayhamlem4  22928  neips  23153  neindisj  23157  ordtrest2lem  23243  lmbrf  23300  lmss  23338  isreg2  23417  lmmo  23420  hauscmplem  23446  bwth  23450  2ndcomap  23498  1stcelcls  23501  restlly  23523  islly2  23524  cldllycmp  23535  comppfsc  23572  1stckgenlem  23593  txbas  23607  txbasval  23646  tx1cn  23649  ptpjopn  23652  ptcnp  23662  txnlly  23677  txlm  23688  xkococn  23700  fgabs  23919  fmfnfmlem4  23997  flimcf  24022  hauspwpwf1  24027  fclsbas  24061  fclscf  24065  flimfnfcls  24068  ghmcnp  24155  tsmsxp  24195  isxmet2d  24367  elmopn2  24485  mopni3  24534  blsscls2  24544  metequiv2  24550  metss2lem  24551  met2ndci  24562  metrest  24564  metcnp  24581  metcnp2  24582  metcnpi3  24586  txmetcnp  24587  nmolb2d  24758  xrge0tsms  24875  metdsre  24894  metnrmlem3  24902  fsumcn  24912  elcncf2  24932  mulc1cncf  24947  cncfco  24949  cncfmet  24951  bndth  25000  evth  25001  copco  25060  pcopt2  25065  pcoass  25066  pcorevlem  25068  lmmcvg  25303  lmmbrf  25304  iscau4  25321  iscauf  25322  cmetcaulem  25330  iscmet3lem3  25332  iscmet3lem1  25333  causs  25340  equivcfil  25341  lmclim  25345  caubl  25350  caublcls  25351  bcth3  25373  ivthle  25498  ivthle2  25499  ovoliunlem1  25544  ovolicc2lem5  25563  volsuplem  25597  uniioombllem6  25630  dyaddisjlem  25637  dyadmax  25640  volcn  25648  mbfmulc2lem  25689  ismbf3d  25696  mbfsup  25706  mbfinf  25707  mbflim  25710  i1fmullem  25736  itg2seq  25784  itg2uba  25785  itg2splitlem  25790  itg2split  25791  itg2monolem1  25792  bddiblnc  25884  ditgsplitlem  25902  ellimc2  25919  ellimc3  25921  limcflf  25923  limcmpt  25925  limcco  25935  lhop1lem  26055  dvfsumle  26063  dvfsumabs  26065  dvfsumrlim  26073  ftc1a  26079  ftc1lem6  26083  mdegmullem  26118  elply2  26236  plypf1  26252  ulmcaulem  26434  ulmcau  26435  ulmss  26437  ulmdvlem3  26442  mtest  26444  itgulm  26448  abelthlem8  26479  abelth  26481  tanord  26580  cxpcn3lem  26789  mcubic  26889  cubic2  26890  dvdsflsumcom  27229  fsumdvdsmul  27236  lgsdchrval  27395  2sqlem9  27468  rplogsumlem2  27526  rpvmasumlem  27528  dchrvmasumlem1  27536  vmalogdivsum2  27579  logsqvma  27583  selberg  27589  selberg4  27602  pntibndlem3  27633  pntlem3  27650  pntleml  27652  padicabv  27671  padicabvf  27672  padicabvcxp  27673  ostth3  27679  nosupbnd1lem5  27753  noinfbnd1lem5  27768  nocvxminlem  27824  lrrecfr  28013  addsprop  28046  mulsproplem9  28194  mulsproplem12  28197  mulsproplem13  28198  mulsproplem14  28199  mulsprop  28200  lemulsd  28208  mulsuniflem  28219  mulsasslem3  28235  axpasch  29088  axcontlem7  29117  axcontlem10  29120  cusgrsize2inds  29600  grpolcan  30679  nvmul0or  30799  nmosetre  30913  blocnilem  30953  blocni  30954  h2hcau  31128  h2hlm  31129  shsel3  31464  chscllem2  31787  homulcl  31908  adjsym  31982  cnvadj  32041  hhcno  32053  hhcnf  32054  lnopl  32063  unoplin  32069  counop  32070  lnfnl  32080  hmoplin  32091  hmopm  32170  nmcexi  32175  lnconi  32182  riesz3i  32211  leopmuli  32282  leopmul  32283  hstle  32379  mdsl0  32459  mdslmd1lem2  32475  atcvatlem  32534  chirredi  32543  cdj1i  32582  sbc2iedf  32612  foresf1o  32652  suppovss  32833  isoun  32854  difioo  32934  swrdf1  33095  xrge0tsmsd  33214  cycpmrn  33284  ressply1invg  33726  ply1unit  33732  fedgmullem2  33888  pstmxmet  34155  ordtrest2NEWlem  34180  esum2dlem  34350  esum2d  34351  dya2icoseg2  34536  eulerpartlemgc  34620  eulerpartlemgh  34636  eulerpartlemgs2  34638  ballotlemimin  34764  signstfvneq0  34830  hgt750lemb  34914  connpconn  35549  cvmliftmolem2  35596  cvmliftlem6  35604  cvmliftlem8  35606  cvmlift2lem12  35628  elmrsubrn  35834  dfon2lem6  36100  ifscgr  36358  brsegle  36422  neibastop2lem  36684  bj-elabd2ALT  37374  bj-ismooredr2  37564  curf  38061  finixpnum  38068  fin2solem  38069  fin2so  38070  lindsenlbs  38078  matunitlindflem1  38079  matunitlindflem2  38080  matunitlindf  38081  poimirlem3  38086  poimirlem4  38087  poimirlem6  38089  poimirlem7  38090  poimirlem14  38097  poimirlem16  38099  poimirlem19  38102  poimirlem22  38105  poimirlem28  38111  poimirlem29  38112  poimirlem30  38113  poimir  38116  heicant  38118  itg2gt0cn  38138  ftc1cnnc  38155  ftc1anclem5  38160  ftc1anclem6  38161  ftc1anclem7  38162  ftc1anc  38164  cover2  38178  filbcmb  38203  fdc  38208  fdc1  38209  seqpo  38210  incsequz  38211  incsequz2  38212  metf1o  38218  lmclim2  38221  geomcau  38222  isbnd2  38246  bndss  38249  ismtybndlem  38269  heibor1lem  38272  rrncmslem  38295  rrnequiv  38298  exidreslem  38340  ghomco  38354  isdrngo3  38422  rngoisocnv  38444  isidlc  38478  idlnegcl  38485  divrngidl  38491  intidl  38492  unichnidl  38494  keridl  38495  igenmin  38527  prnc  38530  ispridlc  38533  erimeq2  39226  prter3  39470  glbconxN  39966  atltcvr  40023  3dim1  40055  lvolnle3at  40170  linepsubN  40340  osumclN  40555  pexmidALTN  40566  lhpmatb  40619  cdlemg1idlemN  41160  dihlss  41838  dihglblem5aN  41880  dihatlat  41922  aks6d1c1p1  42688  aks6d1c5lem1  42717  unitscyglem4  42779  fsuppind  43136  fsuppssindlem1  43137  prjspertr  43151  prjspreln0  43155  lsmfgcl  43615  kercvrlsm  43624  unxpwdom3  43636  hbt  43671  oa0suclim  43816  om0suclim  43817  oe0suclim  43818  naddcnff  43903  cvgdvgrat  44853  climinf  46146  clim2f  46174  clim2cf  46188  clim0cf  46192  clim2f2  46208  fmtnofac2lem  48141  ovmpordxf  48925  oppcthinendcALT  50026  cotsqcscsq  50347  aacllem  50386