Theorem anassrs 468

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anass  469  anass1rs  661  anabss5  674  anabss7  679  mpanr1  709  pm2.61ddan  819  pm2.61dda  820  pm2.61da2ne  3023  ralimdvva  3187  reximdvva  3188  2ralbidva  3202  2rexbidva  3203  2ralbida  3263  spcimgft  3494  copsexgwOLD  5438  copsexg  5439  pofun  5551  imainss  6112  fvmptdf  6949  eqfnfv2  6979  fnex  7168  f1elima  7214  fliftfun  7263  isores2  7284  f1oiso  7302  ovmpodxf  7513  sorpssuni  7682  sorpssint  7683  tfindsg2  7809  2ndconst  8047  mpof1o2d  8072  poxp2  8090  sexp3  8100  poseq  8105  oalim  8464  omlim  8465  oaass  8493  omlimcl  8510  omass  8512  oelim2  8528  oeoa  8530  oeoelem  8531  nnaass  8555  omabs  8584  eroveu  8756  sbthlem4  9025  fimaxg  9194  fisupg  9195  fofinf1o  9239  fiming  9410  fiinfg  9411  ordtypelem7  9436  hartogs  9456  card2on  9466  unwdomg  9496  wemapwe  9616  frmin  9671  dfac5  10049  cfsmolem  10190  isf32lem2  10274  ttukeylem6  10434  ondomon  10483  alephreg  10503  ltexprlem6  10962  recexsrlem  11024  wloglei  11680  recextlem2  11779  fimaxre  12098  creur  12151  uz11  12811  xrmaxeq  13129  xrmineq  13130  xaddf  13174  xaddass  13199  xleadd1a  13203  xlt2add  13210  xmullem  13214  xmulgt0  13233  xmulasslem3  13236  xlemul1a  13238  xadddilem  13244  fzrevral  13564  seqcaopr2  13998  expnlbnd2  14194  faclbnd4lem4  14256  hashgt23el  14384  rtrclreclem3  15020  rtrclreclem4  15021  relexpindlem  15023  rtrclind  15025  shftlem  15028  01sqrex  15209  cau3lem  15315  limsupbnd2  15443  clim2  15464  clim2c  15465  clim0c  15467  rlimresb  15525  2clim  15532  climabs0  15545  climcn1  15552  climcn2  15553  o1rlimmul  15579  climsqz  15601  climsqz2  15602  rlimsqzlem  15609  lo1le  15612  climsup  15630  caucvgrlem2  15635  iseralt  15645  summolem2  15676  fsum2dlem  15730  cvgcmp  15777  cvgcmpce  15779  climfsum  15781  fsumiun  15782  geomulcvg  15839  mertenslem2  15848  mertens  15849  prodfn0  15857  prodfrec  15858  zprod  15900  fprodeq0  15938  fprodn0  15942  fprod2dlem  15943  smu01lem  16452  gcdcllem1  16466  dvdssq  16534  lcmdvds  16575  coprmdvds2  16621  pclem  16807  pcge0  16831  pcgcd1  16846  prmpwdvds  16873  1arithlem4  16895  4sqlem18  16931  vdwlem10  16959  vdwlem11  16960  ramval  16977  ramub1lem2  16996  ramcl  16998  imasaddfnlem  17490  imasaddflem  17492  imasvscafn  17499  imasleval  17503  ismon2  17699  isepi2  17706  issubc3  17814  cofucl  17853  setcmon  18052  setcepi  18053  ipodrsfi  18503  ipodrsima  18505  isacs3lem  18506  grpidpropd  18628  grprida  18641  gsumpropd2lem  18645  mgmhmpropd  18664  mgmhmima  18681  mhmpropd  18758  mhmimalem  18790  grplcan  18974  dfgrp3lem  19012  mulgdirlem  19079  subgmulg  19114  issubg4  19119  subgint  19124  ssnmz  19139  cycsubgcl  19179  gastacl  19282  orbsta  19286  cntzsubg  19312  galactghm  19377  odmulg  19529  odbezout  19531  sylow3lem2  19601  lsmsubm  19626  efgsfo  19712  mulgmhm  19800  mulgghm  19801  gsumval3  19880  gsumcllem  19881  gsumpt  19935  gsum2d  19945  gsum2d2  19947  prdsgsum  19954  subgdmdprd  20009  dprd2d2  20019  ablfac1eu  20048  rngpropd  20153  srglmhm  20200  srgrmhm  20201  ringpropd  20267  ringlghm  20291  pwsgprod  20307  dvdsrpropd  20394  rhmimasubrnglem  20544  cntzsdrg  20781  abvpropd  20814  islmodd  20863  lmodprop2d  20921  lsssubg  20954  lsspropd  21014  lmhmima  21044  lidlsubg  21223  phlpropd  21637  frlmsslsp  21778  lindfmm  21809  islindf4  21820  assapropd  21853  asclpropd  21879  psrass1lem  21915  mplcoe1  22020  mplcoe5  22023  mplind  22053  evlslem2  22062  evlsval  22069  selvvvval  22125  coe1tmmul2  22269  mamuass  22392  mavmulass  22539  mdetuni0  22611  mdetmul  22613  cpmatacl  22706  cpmadugsumfi  22867  cpmadumatpolylem1  22871  cpmadumatpolylem2  22872  cpmadumatpoly  22873  cayhamlem4  22878  neips  23103  neindisj  23107  ordtrest2lem  23193  lmbrf  23250  lmss  23288  isreg2  23367  lmmo  23370  hauscmplem  23396  bwth  23400  2ndcomap  23448  1stcelcls  23451  restlly  23473  islly2  23474  cldllycmp  23485  comppfsc  23522  1stckgenlem  23543  txbas  23557  txbasval  23596  tx1cn  23599  ptpjopn  23602  ptcnp  23612  txnlly  23627  txlm  23638  xkococn  23650  fgabs  23869  fmfnfmlem4  23947  flimcf  23972  hauspwpwf1  23977  fclsbas  24011  fclscf  24015  flimfnfcls  24018  ghmcnp  24105  tsmsxp  24145  isxmet2d  24317  elmopn2  24435  mopni3  24484  blsscls2  24494  metequiv2  24500  metss2lem  24501  met2ndci  24512  metrest  24514  metcnp  24531  metcnp2  24532  metcnpi3  24536  txmetcnp  24537  nmolb2d  24708  xrge0tsms  24825  metdsre  24844  metnrmlem3  24852  fsumcn  24862  elcncf2  24882  mulc1cncf  24897  cncfco  24899  cncfmet  24901  bndth  24950  evth  24951  copco  25010  pcopt2  25015  pcoass  25016  pcorevlem  25018  lmmcvg  25253  lmmbrf  25254  iscau4  25271  iscauf  25272  cmetcaulem  25280  iscmet3lem3  25282  iscmet3lem1  25283  causs  25290  equivcfil  25291  lmclim  25295  caubl  25300  caublcls  25301  bcth3  25323  ivthle  25448  ivthle2  25449  ovoliunlem1  25494  ovolicc2lem5  25513  volsuplem  25547  uniioombllem6  25580  dyaddisjlem  25587  dyadmax  25590  volcn  25598  mbfmulc2lem  25639  ismbf3d  25646  mbfsup  25656  mbfinf  25657  mbflim  25660  i1fmullem  25686  itg2seq  25734  itg2uba  25735  itg2splitlem  25740  itg2split  25741  itg2monolem1  25742  bddiblnc  25834  ditgsplitlem  25852  ellimc2  25869  ellimc3  25871  limcflf  25873  limcmpt  25875  limcco  25885  lhop1lem  26005  dvfsumle  26013  dvfsumabs  26015  dvfsumrlim  26023  ftc1a  26029  ftc1lem6  26033  mdegmullem  26068  elply2  26186  plypf1  26202  ulmcaulem  26384  ulmcau  26385  ulmss  26387  ulmdvlem3  26392  mtest  26394  itgulm  26398  abelthlem8  26429  abelth  26431  tanord  26527  cxpcn3lem  26736  mcubic  26836  cubic2  26837  dvdsflsumcom  27176  fsumdvdsmul  27183  lgsdchrval  27342  2sqlem9  27415  rplogsumlem2  27473  rpvmasumlem  27475  dchrvmasumlem1  27483  vmalogdivsum2  27526  logsqvma  27530  selberg  27536  selberg4  27549  pntibndlem3  27580  pntlem3  27597  pntleml  27599  padicabv  27618  padicabvf  27619  padicabvcxp  27620  ostth3  27626  nosupbnd1lem5  27701  noinfbnd1lem5  27716  nocvxminlem  27771  lrrecfr  27960  addsprop  27993  mulsproplem9  28141  mulsproplem12  28144  mulsproplem13  28145  mulsproplem14  28146  mulsprop  28147  lemulsd  28155  mulsuniflem  28166  mulsasslem3  28182  axpasch  29035  axcontlem7  29064  axcontlem10  29067  cusgrsize2inds  29547  grpolcan  30626  nvmul0or  30746  nmosetre  30860  blocnilem  30900  blocni  30901  h2hcau  31075  h2hlm  31076  shsel3  31411  chscllem2  31734  homulcl  31855  adjsym  31929  cnvadj  31988  hhcno  32000  hhcnf  32001  lnopl  32010  unoplin  32016  counop  32017  lnfnl  32027  hmoplin  32038  hmopm  32117  nmcexi  32122  lnconi  32129  riesz3i  32158  leopmuli  32229  leopmul  32230  hstle  32326  mdsl0  32406  mdslmd1lem2  32422  atcvatlem  32481  chirredi  32490  cdj1i  32529  sbc2iedf  32559  foresf1o  32599  suppovss  32780  isoun  32801  difioo  32881  swrdf1  33042  xrge0tsmsd  33161  cycpmrn  33231  ressply1invg  33659  ply1unit  33665  fedgmullem2  33821  pstmxmet  34088  ordtrest2NEWlem  34113  esum2dlem  34283  esum2d  34284  dya2icoseg2  34469  eulerpartlemgc  34553  eulerpartlemgh  34569  eulerpartlemgs2  34571  ballotlemimin  34697  signstfvneq0  34763  hgt750lemb  34847  connpconn  35470  cvmliftmolem2  35517  cvmliftlem6  35525  cvmliftlem8  35527  cvmlift2lem12  35549  elmrsubrn  35755  dfon2lem6  36021  ifscgr  36279  brsegle  36343  neibastop2lem  36595  bj-elabd2ALT  37285  bj-ismooredr2  37475  curf  37972  finixpnum  37979  fin2solem  37980  fin2so  37981  lindsenlbs  37989  matunitlindflem1  37990  matunitlindflem2  37991  matunitlindf  37992  poimirlem3  37997  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem14  38008  poimirlem16  38010  poimirlem19  38013  poimirlem22  38016  poimirlem28  38022  poimirlem29  38023  poimirlem30  38024  poimir  38027  heicant  38029  itg2gt0cn  38049  ftc1cnnc  38066  ftc1anclem5  38071  ftc1anclem6  38072  ftc1anclem7  38073  ftc1anc  38075  cover2  38089  filbcmb  38114  fdc  38119  fdc1  38120  seqpo  38121  incsequz  38122  incsequz2  38123  metf1o  38129  lmclim2  38132  geomcau  38133  isbnd2  38157  bndss  38160  ismtybndlem  38180  heibor1lem  38183  rrncmslem  38206  rrnequiv  38209  exidreslem  38251  ghomco  38265  isdrngo3  38333  rngoisocnv  38355  isidlc  38389  idlnegcl  38396  divrngidl  38402  intidl  38403  unichnidl  38405  keridl  38406  igenmin  38438  prnc  38441  ispridlc  38444  erimeq2  39137  prter3  39381  glbconxN  39877  atltcvr  39934  3dim1  39966  lvolnle3at  40081  linepsubN  40251  osumclN  40466  pexmidALTN  40477  lhpmatb  40530  cdlemg1idlemN  41071  dihlss  41749  dihglblem5aN  41791  dihatlat  41833  aks6d1c1p1  42599  aks6d1c5lem1  42628  unitscyglem4  42690  fsuppind  43047  fsuppssindlem1  43048  prjspertr  43062  prjspreln0  43066  lsmfgcl  43526  kercvrlsm  43535  unxpwdom3  43547  hbt  43582  oa0suclim  43727  om0suclim  43728  oe0suclim  43729  naddcnff  43814  cvgdvgrat  44764  climinf  46058  clim2f  46086  clim2cf  46100  clim0cf  46104  clim2f2  46120  fmtnofac2lem  48053  ovmpordxf  48837  oppcthinendcALT  49938  cotsqcscsq  50259  aacllem  50298