Theorem anassrs 473

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anass  474  anass1rs  668  anabss5  681  anabss7  686  mpanr1  716  pm2.61ddan  826  pm2.61dda  827  pm2.61da2ne  3044  ralimdvva  3210  reximdvva  3211  2ralbidva  3225  2rexbidva  3226  2ralbida  3286  spcimgft  3511  copsexgwOLD  5461  copsexg  5462  pofun  5577  imainss  6143  fvmptdf  6992  eqfnfv2  7022  fnex  7215  f1elima  7259  fliftfun  7312  isores2  7333  f1oiso  7351  ovmpodxf  7562  sorpssuni  7737  sorpssint  7738  tfindsg2  7862  2ndconst  8101  mpof1o2d  8126  poxp2  8144  sexp3  8154  poseq  8159  oalim  8524  omlim  8525  oaass  8553  omlimcl  8570  omass  8572  oelim2  8588  oeoa  8590  oeoelem  8591  nnaass  8615  omabs  8644  eroveu  8817  curf  8874  sbthlem4  9093  fimaxg  9262  fisupg  9263  fofinf1o  9305  fiming  9476  fiinfg  9477  ordtypelem7  9502  hartogs  9522  card2on  9532  unwdomg  9562  wemapwe  9682  frmin  9737  dfac5  10188  cfsmolem  10329  isf32lem2  10413  ttukeylem6  10573  ondomon  10628  alephreg  10648  ltexprlem6  11107  recexsrlem  11169  wloglei  11829  recextlem2  11928  fimaxre  12242  creur  12295  uz11  12971  xrmaxeq  13290  xrmineq  13291  xaddf  13335  xaddass  13360  xleadd1a  13364  xlt2add  13371  xmullem  13375  xmulgt0  13394  xmulasslem3  13397  xlemul1a  13399  xadddilem  13405  fzrevral  13726  seqcaopr2  14161  expnlbnd2  14358  faclbnd4lem4  14420  hashgt23el  14549  swrdf1  14779  rtrclreclem3  15193  rtrclreclem4  15194  relexpindlem  15196  rtrclind  15198  shftlem  15201  01sqrex  15396  cau3lem  15502  limsupbnd2  15630  clim2  15651  clim2c  15652  clim0c  15654  rlimresb  15712  2clim  15719  climabs0  15732  climcn1  15739  climcn2  15740  o1rlimmul  15766  climsqz  15788  climsqz2  15789  rlimsqzlem  15796  lo1le  15799  climsup  15817  caucvgrlem2  15822  iseralt  15832  summolem2  15862  fsum2dlem  15916  cvgcmp  15963  cvgcmpce  15965  climfsum  15967  fsumiun  15968  geomulcvg  16025  mertenslem2  16034  mertens  16035  prodfn0  16043  prodfrec  16044  zprod  16084  fprodeq0  16122  fprodn0  16126  fprod2dlem  16127  smu01lem  16635  gcdcllem1  16649  dvdssq  16722  lcmdvds  16763  coprmdvds2  16809  pclem  16996  pcge0  17020  pcgcd1  17035  prmpwdvds  17062  1arithlem4  17084  4sqlem18  17120  vdwlem10  17148  vdwlem11  17149  ramval  17166  ramub1lem2  17185  ramcl  17187  imasaddfnlem  17680  imasaddflem  17682  imasvscafn  17689  imasleval  17693  ismon2  17889  isepi2  17896  issubc3  18004  cofucl  18043  setcmon  18242  setcepi  18243  ipodrsfi  18693  ipodrsima  18695  isacs3lem  18696  grpidpropd  18822  grprida  18836  gsumpropd2lem  18848  mgmhmpropd  18867  mgmhmima  18884  mhmpropd  18967  mhmimalem  19000  grplcan  19191  dfgrp3lem  19228  mulgdirlem  19295  subgmulg  19331  issubg4  19336  subgint  19341  ssnmz  19356  cycsubgcl  19401  gastacl  19503  orbsta  19507  cntzsubg  19533  galactghm  19598  odmulg  19750  odbezout  19752  sylow3lem2  19822  lsmsubm  19847  efgsfo  19933  mulgmhm  20021  mulgghm  20022  gsumval3  20101  gsumcllem  20102  gsumpt  20156  gsum2d  20166  gsum2d2  20168  prdsgsum  20175  subgdmdprd  20230  dprd2d2  20240  ablfac1eu  20269  rngpropd  20376  srglmhm  20427  srgrmhm  20428  ringpropd  20499  ringlghm  20523  pwsgprod  20539  dvdsrpropd  20626  rhmimasubrnglem  20797  isdrng5  20988  cntzsdrg  21039  abvpropd  21072  islmodd  21121  lmodprop2d  21179  lsssubg  21212  lsspropd  21272  lmhmima  21302  lidlsubg  21482  phlpropd  21941  frlmsslsp  22082  lindfmm  22113  islindf4  22124  lindsenlbs  22137  assapropd  22159  asclpropd  22185  psrass1lem  22221  mplcoe1  22326  mplcoe5  22329  mplind  22359  evlslem2  22368  evlsval  22375  selvvvval  22431  coe1tmmul2  22575  mamuass  22697  mavmulass  22844  mdetuni0  22916  mdetmul  22918  matunitlindflem1  22974  matunitlindflem2  22975  matunitlindf  22976  cpmatacl  23014  cpmadugsumfi  23175  cpmadumatpolylem1  23179  cpmadumatpolylem2  23180  cpmadumatpoly  23181  cayhamlem4  23186  neips  23411  neindisj  23415  ordtrest2lem  23501  lmbrf  23558  lmss  23596  isreg2  23675  lmmo  23678  hauscmplem  23704  bwth  23708  2ndcomap  23757  1stcelcls  23760  restlly  23782  islly2  23783  cldllycmp  23794  comppfsc  23831  1stckgenlem  23852  txbas  23866  txbasval  23905  tx1cn  23908  ptpjopn  23911  ptcnp  23921  txnlly  23936  txlm  23947  xkococn  23959  fgabs  24178  fmfnfmlem4  24256  flimcf  24281  hauspwpwf1  24286  fclsbas  24320  fclscf  24324  flimfnfcls  24327  ghmcnp  24414  tsmsxp  24454  isxmet2d  24626  elmopn2  24744  mopni3  24793  blsscls2  24803  metequiv2  24809  metss2lem  24810  met2ndci  24821  metrest  24823  metcnp  24840  metcnp2  24841  metcnpi3  24845  txmetcnp  24846  nmolb2d  25017  xrge0tsms  25134  metdsre  25153  metnrmlem3  25161  fsumcn  25171  elcncf2  25191  mulc1cncf  25206  cncfco  25208  cncfmet  25210  bndth  25259  evth  25260  copco  25319  pcopt2  25324  pcoass  25325  pcorevlem  25327  lmmcvg  25562  lmmbrf  25563  iscau4  25580  iscauf  25581  cmetcaulem  25589  iscmet3lem3  25591  iscmet3lem1  25592  causs  25599  equivcfil  25600  lmclim  25604  caubl  25609  caublcls  25610  bcth3  25632  ivthle  25757  ivthle2  25758  ovoliunlem1  25803  ovolicc2lem5  25822  volsuplem  25856  uniioombllem6  25889  dyaddisjlem  25896  dyadmax  25899  volcn  25907  mbfmulc2lem  25948  ismbf3d  25955  mbfsup  25965  mbfinf  25966  mbflim  25969  i1fmullem  25995  itg2seq  26043  itg2uba  26044  itg2splitlem  26049  itg2split  26050  itg2monolem1  26051  bddiblnc  26142  ditgsplitlem  26160  ellimc2  26177  ellimc3  26179  limcflf  26181  limcmpt  26183  limcco  26193  lhop1lem  26313  dvfsumle  26321  dvfsumabs  26323  dvfsumrlim  26331  ftc1a  26337  ftc1lem6  26341  mdegmullem  26376  elply2  26494  plypf1  26511  ulmcaulem  26703  ulmcau  26704  ulmss  26706  ulmdvlem3  26711  mtest  26713  itgulm  26717  abelthlem8  26748  abelth  26750  tanord  26848  cxpcn3lem  27057  mcubic  27157  cubic2  27158  dvdsflsumcom  27497  fsumdvdsmul  27504  lgsdchrval  27663  2sqlem9  27736  rplogsumlem2  27794  rpvmasumlem  27796  dchrvmasumlem1  27804  vmalogdivsum2  27847  logsqvma  27851  selberg  27857  selberg4  27870  pntibndlem3  27901  pntlem3  27918  pntleml  27920  padicabv  27939  padicabvf  27940  padicabvcxp  27941  ostth3  27947  nosupbnd1lem5  28051  noinfbnd1lem5  28066  nocvxminlem  28122  lrrecfr  28311  addsprop  28344  mulsproplem9  28492  mulsproplem12  28495  mulsproplem13  28496  mulsproplem14  28497  mulsprop  28498  lemulsd  28506  mulsuniflem  28517  mulsasslem3  28533  axpasch  29501  axcontlem7  29530  axcontlem10  29533  cusgrsize2inds  30016  grpolcan  31114  nvmul0or  31234  nmosetre  31348  blocnilem  31388  blocni  31389  h2hcau  31563  h2hlm  31564  shsel3  31899  chscllem2  32222  homulcl  32343  adjsym  32417  cnvadj  32476  hhcno  32488  hhcnf  32489  lnopl  32498  unoplin  32504  counop  32505  lnfnl  32515  hmoplin  32526  hmopm  32605  nmcexi  32610  lnconi  32617  riesz3i  32646  leopmuli  32717  leopmul  32718  hstle  32814  mdsl0  32894  mdslmd1lem2  32910  atcvatlem  32969  chirredi  32978  cdj1i  33017  sbc2iedf  33044  foresf1o  33082  suppovss  33256  isoun  33277  difioo  33356  xrge0tsmsd  33616  cycpmrn  33686  ressply1invg  34083  ply1unit  34089  fedgmullem2  34244  pstmxmet  34511  ordtrest2NEWlem  34536  esum2dlem  34706  esum2d  34707  dya2icoseg2  34893  eulerpartlemgc  34977  eulerpartlemgh  34993  eulerpartlemgs2  34995  ballotlemimin  35121  signstfvneq0  35184  hgt750lemb  35268  connpconn  35969  cvmliftmolem2  36016  cvmliftlem6  36024  cvmliftlem8  36026  cvmlift2lem12  36048  elmrsubrn  36254  dfon2lem6  36520  ifscgr  36779  brsegle  36843  neibastop2lem  37118  bj-elabd2ALT  37808  bj-ismooredr2  37999  finixpnum  38496  fin2solem  38497  fin2so  38498  poimirlem3  38509  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem14  38520  poimirlem16  38522  poimirlem19  38525  poimirlem22  38528  poimirlem28  38534  poimirlem29  38535  poimirlem30  38536  poimir  38539  heicant  38541  itg2gt0cn  38561  ftc1cnnc  38578  ftc1anclem5  38583  ftc1anclem6  38584  ftc1anclem7  38585  ftc1anc  38587  cover2  38617  filbcmb  38642  fdc  38647  fdc1  38648  seqpo  38649  incsequz  38650  incsequz2  38651  metf1o  38657  lmclim2  38660  geomcau  38661  isbnd2  38685  bndss  38688  ismtybndlem  38708  heibor1lem  38711  rrncmslem  38734  rrnequiv  38737  exidreslem  38779  ghomco  38793  isdrngo3  38861  rngoisocnv  38883  isidlc  38917  idlnegcl  38924  divrngidl  38930  intidl  38931  unichnidl  38933  keridl  38934  igenmin  38966  prnc  38969  ispridlc  38972  erimeq2  39663  prter3  39907  glbconxN  40403  atltcvr  40460  3dim1  40492  lvolnle3at  40607  linepsubN  40777  osumclN  40992  pexmidALTN  41003  lhpmatb  41056  cdlemg1idlemN  41597  dihlss  42275  dihglblem5aN  42317  dihatlat  42359  aks6d1c1p1  43125  aks6d1c5lem1  43154  unitscyglem4  43216  fsuppind  43580  fsuppssindlem1  43581  prjspertr  43595  prjspreln0  43599  lsmfgcl  44034  kercvrlsm  44043  unxpwdom3  44055  hbt  44090  oa0suclim  44235  om0suclim  44236  oe0suclim  44237  naddcnff  44322  cvgdvgrat  45256  climinf  46562  clim2f  46590  clim2cf  46604  clim0cf  46608  clim2f2  46624  fmtnofac2lem  48597  ovmpordxf  49395  oppcthinendcALT  50493  cotsqcscsq  50799  aacllem  50883