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  3046  ralimdvva  3212  reximdvva  3213  2ralbidva  3227  2rexbidva  3228  2ralbida  3288  spcimgft  3515  copsexgwOLD  5475  copsexg  5476  pofun  5589  imainss  6153  fvmptdf  6998  eqfnfv2  7028  fnex  7217  f1elima  7263  fliftfun  7312  isores2  7333  f1oiso  7351  ovmpodxf  7562  sorpssuni  7731  sorpssint  7732  tfindsg2  7859  2ndconst  8097  mpof1o2d  8122  poxp2  8140  sexp3  8150  poseq  8155  oalim  8518  omlim  8519  oaass  8547  omlimcl  8564  omass  8566  oelim2  8582  oeoa  8584  oeoelem  8585  nnaass  8609  omabs  8638  eroveu  8811  sbthlem4  9079  fimaxg  9248  fisupg  9249  fofinf1o  9290  fiming  9461  fiinfg  9462  ordtypelem7  9487  hartogs  9507  card2on  9517  unwdomg  9547  wemapwe  9667  frmin  9722  dfac5  10113  cfsmolem  10255  isf32lem2  10339  ttukeylem6  10499  ondomon  10548  alephreg  10568  ltexprlem6  11027  recexsrlem  11089  wloglei  11747  recextlem2  11846  fimaxre  12160  creur  12213  uz11  12888  xrmaxeq  13206  xrmineq  13207  xaddf  13251  xaddass  13276  xleadd1a  13280  xlt2add  13287  xmullem  13291  xmulgt0  13310  xmulasslem3  13313  xlemul1a  13315  xadddilem  13321  fzrevral  13642  seqcaopr2  14076  expnlbnd2  14272  faclbnd4lem4  14334  hashgt23el  14463  rtrclreclem3  15099  rtrclreclem4  15100  relexpindlem  15102  rtrclind  15104  shftlem  15107  01sqrex  15302  cau3lem  15408  limsupbnd2  15536  clim2  15557  clim2c  15558  clim0c  15560  rlimresb  15618  2clim  15625  climabs0  15638  climcn1  15645  climcn2  15646  o1rlimmul  15672  climsqz  15694  climsqz2  15695  rlimsqzlem  15702  lo1le  15705  climsup  15723  caucvgrlem2  15728  iseralt  15738  summolem2  15769  fsum2dlem  15823  cvgcmp  15870  cvgcmpce  15872  climfsum  15874  fsumiun  15875  geomulcvg  15932  mertenslem2  15941  mertens  15942  prodfn0  15950  prodfrec  15951  zprod  15993  fprodeq0  16031  fprodn0  16035  fprod2dlem  16036  smu01lem  16544  gcdcllem1  16558  dvdssq  16626  lcmdvds  16667  coprmdvds2  16713  pclem  16899  pcge0  16923  pcgcd1  16938  prmpwdvds  16965  1arithlem4  16987  4sqlem18  17023  vdwlem10  17051  vdwlem11  17052  ramval  17069  ramub1lem2  17088  ramcl  17090  imasaddfnlem  17583  imasaddflem  17585  imasvscafn  17592  imasleval  17596  ismon2  17792  isepi2  17799  issubc3  17907  cofucl  17946  setcmon  18145  setcepi  18146  ipodrsfi  18596  ipodrsima  18598  isacs3lem  18599  grpidpropd  18721  grprida  18734  gsumpropd2lem  18738  mgmhmpropd  18757  mgmhmima  18774  mhmpropd  18851  mhmimalem  18884  grplcan  19068  dfgrp3lem  19105  mulgdirlem  19172  subgmulg  19208  issubg4  19213  subgint  19218  ssnmz  19233  cycsubgcl  19278  gastacl  19380  orbsta  19384  cntzsubg  19410  galactghm  19475  odmulg  19627  odbezout  19629  sylow3lem2  19699  lsmsubm  19724  efgsfo  19810  mulgmhm  19898  mulgghm  19899  gsumval3  19978  gsumcllem  19979  gsumpt  20033  gsum2d  20043  gsum2d2  20045  prdsgsum  20052  subgdmdprd  20107  dprd2d2  20117  ablfac1eu  20146  rngpropd  20253  srglmhm  20304  srgrmhm  20305  ringpropd  20372  ringlghm  20396  pwsgprod  20412  dvdsrpropd  20499  rhmimasubrnglem  20651  cntzsdrg  20886  abvpropd  20919  islmodd  20968  lmodprop2d  21026  lsssubg  21059  lsspropd  21119  lmhmima  21149  lidlsubg  21329  phlpropd  21786  frlmsslsp  21927  lindfmm  21958  islindf4  21969  assapropd  22002  asclpropd  22028  psrass1lem  22064  mplcoe1  22169  mplcoe5  22172  mplind  22202  evlslem2  22211  evlsval  22218  selvvvval  22274  coe1tmmul2  22418  mamuass  22540  mavmulass  22687  mdetuni0  22759  mdetmul  22761  cpmatacl  22854  cpmadugsumfi  23015  cpmadumatpolylem1  23019  cpmadumatpolylem2  23020  cpmadumatpoly  23021  cayhamlem4  23026  neips  23251  neindisj  23255  ordtrest2lem  23341  lmbrf  23398  lmss  23436  isreg2  23515  lmmo  23518  hauscmplem  23544  bwth  23548  2ndcomap  23596  1stcelcls  23599  restlly  23621  islly2  23622  cldllycmp  23633  comppfsc  23670  1stckgenlem  23691  txbas  23705  txbasval  23744  tx1cn  23747  ptpjopn  23750  ptcnp  23760  txnlly  23775  txlm  23786  xkococn  23798  fgabs  24017  fmfnfmlem4  24095  flimcf  24120  hauspwpwf1  24125  fclsbas  24159  fclscf  24163  flimfnfcls  24166  ghmcnp  24253  tsmsxp  24293  isxmet2d  24465  elmopn2  24583  mopni3  24632  blsscls2  24642  metequiv2  24648  metss2lem  24649  met2ndci  24660  metrest  24662  metcnp  24679  metcnp2  24680  metcnpi3  24684  txmetcnp  24685  nmolb2d  24856  xrge0tsms  24973  metdsre  24992  metnrmlem3  25000  fsumcn  25010  elcncf2  25030  mulc1cncf  25045  cncfco  25047  cncfmet  25049  bndth  25098  evth  25099  copco  25158  pcopt2  25163  pcoass  25164  pcorevlem  25166  lmmcvg  25401  lmmbrf  25402  iscau4  25419  iscauf  25420  cmetcaulem  25428  iscmet3lem3  25430  iscmet3lem1  25431  causs  25438  equivcfil  25439  lmclim  25443  caubl  25448  caublcls  25449  bcth3  25471  ivthle  25596  ivthle2  25597  ovoliunlem1  25642  ovolicc2lem5  25661  volsuplem  25695  uniioombllem6  25728  dyaddisjlem  25735  dyadmax  25738  volcn  25746  mbfmulc2lem  25787  ismbf3d  25794  mbfsup  25804  mbfinf  25805  mbflim  25808  i1fmullem  25834  itg2seq  25882  itg2uba  25883  itg2splitlem  25888  itg2split  25889  itg2monolem1  25890  bddiblnc  25982  ditgsplitlem  26000  ellimc2  26017  ellimc3  26019  limcflf  26021  limcmpt  26023  limcco  26033  lhop1lem  26153  dvfsumle  26161  dvfsumabs  26163  dvfsumrlim  26171  ftc1a  26177  ftc1lem6  26181  mdegmullem  26216  elply2  26334  plypf1  26350  ulmcaulem  26538  ulmcau  26539  ulmss  26541  ulmdvlem3  26546  mtest  26548  itgulm  26552  abelthlem8  26583  abelth  26585  tanord  26684  cxpcn3lem  26893  mcubic  26993  cubic2  26994  dvdsflsumcom  27333  fsumdvdsmul  27340  lgsdchrval  27499  2sqlem9  27572  rplogsumlem2  27630  rpvmasumlem  27632  dchrvmasumlem1  27640  vmalogdivsum2  27683  logsqvma  27687  selberg  27693  selberg4  27706  pntibndlem3  27737  pntlem3  27754  pntleml  27756  padicabv  27775  padicabvf  27776  padicabvcxp  27777  ostth3  27783  nosupbnd1lem5  27857  noinfbnd1lem5  27872  nocvxminlem  27928  lrrecfr  28117  addsprop  28150  mulsproplem9  28298  mulsproplem12  28301  mulsproplem13  28302  mulsproplem14  28303  mulsprop  28304  lemulsd  28312  mulsuniflem  28323  mulsasslem3  28339  axpasch  29272  axcontlem7  29301  axcontlem10  29304  cusgrsize2inds  29784  grpolcan  30863  nvmul0or  30983  nmosetre  31097  blocnilem  31137  blocni  31138  h2hcau  31312  h2hlm  31313  shsel3  31648  chscllem2  31971  homulcl  32092  adjsym  32166  cnvadj  32225  hhcno  32237  hhcnf  32238  lnopl  32247  unoplin  32253  counop  32254  lnfnl  32264  hmoplin  32275  hmopm  32354  nmcexi  32359  lnconi  32366  riesz3i  32395  leopmuli  32466  leopmul  32467  hstle  32563  mdsl0  32643  mdslmd1lem2  32659  atcvatlem  32718  chirredi  32727  cdj1i  32766  sbc2iedf  32793  foresf1o  32831  suppovss  33007  isoun  33028  difioo  33108  swrdf1  33257  xrge0tsmsd  33374  cycpmrn  33444  ressply1invg  33840  ply1unit  33846  fedgmullem2  34001  pstmxmet  34268  ordtrest2NEWlem  34293  esum2dlem  34463  esum2d  34464  dya2icoseg2  34649  eulerpartlemgc  34733  eulerpartlemgh  34749  eulerpartlemgs2  34751  ballotlemimin  34877  signstfvneq0  34940  hgt750lemb  35024  connpconn  35708  cvmliftmolem2  35755  cvmliftlem6  35763  cvmliftlem8  35765  cvmlift2lem12  35787  elmrsubrn  35993  dfon2lem6  36259  ifscgr  36517  brsegle  36581  neibastop2lem  36852  bj-elabd2ALT  37542  bj-ismooredr2  37733  curf  38230  finixpnum  38237  fin2solem  38238  fin2so  38239  lindsenlbs  38247  matunitlindflem1  38248  matunitlindflem2  38249  matunitlindf  38250  poimirlem3  38255  poimirlem4  38256  poimirlem6  38258  poimirlem7  38259  poimirlem14  38266  poimirlem16  38268  poimirlem19  38271  poimirlem22  38274  poimirlem28  38280  poimirlem29  38281  poimirlem30  38282  poimir  38285  heicant  38287  itg2gt0cn  38307  ftc1cnnc  38324  ftc1anclem5  38329  ftc1anclem6  38330  ftc1anclem7  38331  ftc1anc  38333  cover2  38347  filbcmb  38372  fdc  38377  fdc1  38378  seqpo  38379  incsequz  38380  incsequz2  38381  metf1o  38387  lmclim2  38390  geomcau  38391  isbnd2  38415  bndss  38418  ismtybndlem  38438  heibor1lem  38441  rrncmslem  38464  rrnequiv  38467  exidreslem  38509  ghomco  38523  isdrngo3  38591  rngoisocnv  38613  isidlc  38647  idlnegcl  38654  divrngidl  38660  intidl  38661  unichnidl  38663  keridl  38664  igenmin  38696  prnc  38699  ispridlc  38702  erimeq2  39393  prter3  39637  glbconxN  40133  atltcvr  40190  3dim1  40222  lvolnle3at  40337  linepsubN  40507  osumclN  40722  pexmidALTN  40733  lhpmatb  40786  cdlemg1idlemN  41327  dihlss  42005  dihglblem5aN  42047  dihatlat  42089  aks6d1c1p1  42855  aks6d1c5lem1  42884  unitscyglem4  42946  fsuppind  43305  fsuppssindlem1  43306  prjspertr  43320  prjspreln0  43324  lsmfgcl  43784  kercvrlsm  43793  unxpwdom3  43805  hbt  43840  oa0suclim  43985  om0suclim  43986  oe0suclim  43987  naddcnff  44072  cvgdvgrat  45006  climinf  46305  clim2f  46333  clim2cf  46347  clim0cf  46351  clim2f2  46367  fmtnofac2lem  48303  ovmpordxf  49102  oppcthinendcALT  50202  cotsqcscsq  50523  aacllem  50584