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  813  pm2.61dda  814  pm2.61da2ne  3013  ralimdvva  3176  reximdvva  3177  2ralbidva  3191  2rexbidva  3192  2ralbida  3252  spcimgft  3503  copsexgw  5437  copsexg  5438  pofun  5549  imainss  6107  fvmptdf  6940  eqfnfv2  6970  fnex  7157  f1elima  7204  fliftfun  7253  isores2  7274  f1oiso  7292  ovmpodxf  7503  sorpssuni  7672  sorpssint  7673  tfindsg2  7802  2ndconst  8041  poxp2  8083  sexp3  8093  poseq  8098  oalim  8457  omlim  8458  oaass  8486  omlimcl  8503  omass  8505  oelim2  8520  oeoa  8522  oeoelem  8523  nnaass  8547  omabs  8576  eroveu  8746  sbthlem4  9014  fimaxg  9192  fisupg  9193  fofinf1o  9241  fiming  9409  fiinfg  9410  ordtypelem7  9435  hartogs  9455  card2on  9465  unwdomg  9495  wemapwe  9612  frmin  9664  dfac5  10042  cfsmolem  10183  isf32lem2  10267  ttukeylem6  10427  ondomon  10476  alephreg  10495  ltexprlem6  10954  recexsrlem  11016  wloglei  11670  recextlem2  11769  fimaxre  12087  creur  12140  uz11  12778  xrmaxeq  13099  xrmineq  13100  xaddf  13144  xaddass  13169  xleadd1a  13173  xlt2add  13180  xmullem  13184  xmulgt0  13203  xmulasslem3  13206  xlemul1a  13208  xadddilem  13214  fzrevral  13533  seqcaopr2  13963  expnlbnd2  14159  faclbnd4lem4  14221  hashgt23el  14349  rtrclreclem3  14985  rtrclreclem4  14986  relexpindlem  14988  rtrclind  14990  shftlem  14993  01sqrex  15174  cau3lem  15280  limsupbnd2  15408  clim2  15429  clim2c  15430  clim0c  15432  rlimresb  15490  2clim  15497  climabs0  15510  climcn1  15517  climcn2  15518  o1rlimmul  15544  climsqz  15566  climsqz2  15567  rlimsqzlem  15574  lo1le  15577  climsup  15595  caucvgrlem2  15600  iseralt  15610  summolem2  15641  fsum2dlem  15695  cvgcmp  15741  cvgcmpce  15743  climfsum  15745  fsumiun  15746  geomulcvg  15801  mertenslem2  15810  mertens  15811  prodfn0  15819  prodfrec  15820  zprod  15862  fprodeq0  15900  fprodn0  15904  fprod2dlem  15905  smu01lem  16414  gcdcllem1  16428  dvdssq  16496  lcmdvds  16537  coprmdvds2  16583  pclem  16768  pcge0  16792  pcgcd1  16807  prmpwdvds  16834  1arithlem4  16856  4sqlem18  16892  vdwlem10  16920  vdwlem11  16921  ramval  16938  ramub1lem2  16957  ramcl  16959  imasaddfnlem  17450  imasaddflem  17452  imasvscafn  17459  imasleval  17463  ismon2  17659  isepi2  17666  issubc3  17774  cofucl  17813  setcmon  18012  setcepi  18013  ipodrsfi  18463  ipodrsima  18465  isacs3lem  18466  grpidpropd  18554  grprida  18567  gsumpropd2lem  18571  mgmhmpropd  18590  mgmhmima  18607  mhmpropd  18684  mhmimalem  18716  grplcan  18897  dfgrp3lem  18935  mulgdirlem  19002  subgmulg  19037  issubg4  19042  subgint  19047  ssnmz  19063  cycsubgcl  19103  gastacl  19206  orbsta  19210  cntzsubg  19236  galactghm  19301  odmulg  19453  odbezout  19455  sylow3lem2  19525  lsmsubm  19550  efgsfo  19636  mulgmhm  19724  mulgghm  19725  gsumval3  19804  gsumcllem  19805  gsumpt  19859  gsum2d  19869  gsum2d2  19871  prdsgsum  19878  subgdmdprd  19933  dprd2d2  19943  ablfac1eu  19972  rngpropd  20077  srglmhm  20124  srgrmhm  20125  ringpropd  20191  ringlghm  20215  dvdsrpropd  20319  rhmimasubrnglem  20468  cntzsdrg  20705  abvpropd  20738  islmodd  20787  lmodprop2d  20845  lsssubg  20878  lsspropd  20939  lmhmima  20969  lidlsubg  21148  phlpropd  21580  frlmsslsp  21721  lindfmm  21752  islindf4  21763  assapropd  21797  asclpropd  21822  psrass1lem  21857  mplcoe1  21960  mplcoe5  21963  mplind  21993  evlslem2  22002  evlsval  22009  coe1tmmul2  22178  mamuass  22305  mavmulass  22452  mdetuni0  22524  mdetmul  22526  cpmatacl  22619  cpmadugsumfi  22780  cpmadumatpolylem1  22784  cpmadumatpolylem2  22785  cpmadumatpoly  22786  cayhamlem4  22791  neips  23016  neindisj  23020  ordtrest2lem  23106  lmbrf  23163  lmss  23201  isreg2  23280  lmmo  23283  hauscmplem  23309  bwth  23313  2ndcomap  23361  1stcelcls  23364  restlly  23386  islly2  23387  cldllycmp  23398  comppfsc  23435  1stckgenlem  23456  txbas  23470  txbasval  23509  tx1cn  23512  ptpjopn  23515  ptcnp  23525  txnlly  23540  txlm  23551  xkococn  23563  fgabs  23782  fmfnfmlem4  23860  flimcf  23885  hauspwpwf1  23890  fclsbas  23924  fclscf  23928  flimfnfcls  23931  ghmcnp  24018  tsmsxp  24058  isxmet2d  24231  elmopn2  24349  mopni3  24398  blsscls2  24408  metequiv2  24414  metss2lem  24415  met2ndci  24426  metrest  24428  metcnp  24445  metcnp2  24446  metcnpi3  24450  txmetcnp  24451  nmolb2d  24622  xrge0tsms  24739  metdsre  24758  metnrmlem3  24766  fsumcn  24777  elcncf2  24799  mulc1cncf  24814  cncfco  24816  cncfmet  24818  bndth  24873  evth  24874  copco  24934  pcopt2  24939  pcoass  24940  pcorevlem  24942  lmmcvg  25177  lmmbrf  25178  iscau4  25195  iscauf  25196  cmetcaulem  25204  iscmet3lem3  25206  iscmet3lem1  25207  causs  25214  equivcfil  25215  lmclim  25219  caubl  25224  caublcls  25225  bcth3  25247  ivthle  25373  ivthle2  25374  ovoliunlem1  25419  ovolicc2lem5  25438  volsuplem  25472  uniioombllem6  25505  dyaddisjlem  25512  dyadmax  25515  volcn  25523  mbfmulc2lem  25564  ismbf3d  25571  mbfsup  25581  mbfinf  25582  mbflim  25585  i1fmullem  25611  itg2seq  25659  itg2uba  25660  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  bddiblnc  25759  ditgsplitlem  25777  ellimc2  25794  ellimc3  25796  limcflf  25798  limcmpt  25800  limcco  25810  lhop1lem  25934  dvfsumle  25942  dvfsumleOLD  25943  dvfsumabs  25945  dvfsumrlim  25954  ftc1a  25960  ftc1lem6  25964  mdegmullem  25999  elply2  26117  plypf1  26133  ulmcaulem  26319  ulmcau  26320  ulmss  26322  ulmdvlem3  26327  mtest  26329  itgulm  26333  abelthlem8  26365  abelth  26367  tanord  26463  cxpcn3lem  26673  mcubic  26773  cubic2  26774  dvdsflsumcom  27114  fsumdvdsmul  27121  fsumdvdsmulOLD  27123  lgsdchrval  27281  2sqlem9  27354  rplogsumlem2  27412  rpvmasumlem  27414  dchrvmasumlem1  27422  vmalogdivsum2  27465  logsqvma  27469  selberg  27475  selberg4  27488  pntibndlem3  27519  pntlem3  27536  pntleml  27538  padicabv  27557  padicabvf  27558  padicabvcxp  27559  ostth3  27565  nosupbnd1lem5  27640  noinfbnd1lem5  27655  nocvxminlem  27706  lrrecfr  27873  addsprop  27906  mulsproplem9  28050  mulsproplem12  28053  mulsproplem13  28054  mulsproplem14  28055  mulsprop  28056  slemuld  28064  mulsuniflem  28075  mulsasslem3  28091  axpasch  28904  axcontlem7  28933  axcontlem10  28936  cusgrsize2inds  29417  grpolcan  30492  nvmul0or  30612  nmosetre  30726  blocnilem  30766  blocni  30767  h2hcau  30941  h2hlm  30942  shsel3  31277  chscllem2  31600  homulcl  31721  adjsym  31795  cnvadj  31854  hhcno  31866  hhcnf  31867  lnopl  31876  unoplin  31882  counop  31883  lnfnl  31893  hmoplin  31904  hmopm  31983  nmcexi  31988  lnconi  31995  riesz3i  32024  leopmuli  32095  leopmul  32096  hstle  32192  mdsl0  32272  mdslmd1lem2  32288  atcvatlem  32347  chirredi  32356  cdj1i  32395  sbc2iedf  32427  foresf1o  32466  suppovss  32637  isoun  32658  difioo  32738  swrdf1  32911  xrge0tsmsd  33028  cycpmrn  33098  ressply1invg  33514  ply1unit  33520  fedgmullem2  33602  pstmxmet  33863  ordtrest2NEWlem  33888  esum2dlem  34058  esum2d  34059  dya2icoseg2  34245  eulerpartlemgc  34329  eulerpartlemgh  34345  eulerpartlemgs2  34347  ballotlemimin  34473  signstfvneq0  34539  hgt750lemb  34623  connpconn  35207  cvmliftmolem2  35254  cvmliftlem6  35262  cvmliftlem8  35264  cvmlift2lem12  35286  elmrsubrn  35492  dfon2lem6  35761  ifscgr  36017  brsegle  36081  neibastop2lem  36333  bj-elabd2ALT  36898  bj-ismooredr2  37083  curf  37577  finixpnum  37584  fin2solem  37585  fin2so  37586  lindsenlbs  37594  matunitlindflem1  37595  matunitlindflem2  37596  matunitlindf  37597  poimirlem3  37602  poimirlem4  37603  poimirlem6  37605  poimirlem7  37606  poimirlem14  37613  poimirlem16  37615  poimirlem19  37618  poimirlem22  37621  poimirlem28  37627  poimirlem29  37628  poimirlem30  37629  poimir  37632  heicant  37634  itg2gt0cn  37654  ftc1cnnc  37671  ftc1anclem5  37676  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anc  37680  cover2  37694  filbcmb  37719  fdc  37724  fdc1  37725  seqpo  37726  incsequz  37727  incsequz2  37728  metf1o  37734  lmclim2  37737  geomcau  37738  isbnd2  37762  bndss  37765  ismtybndlem  37785  heibor1lem  37788  rrncmslem  37811  rrnequiv  37814  exidreslem  37856  ghomco  37870  isdrngo3  37938  rngoisocnv  37960  isidlc  37994  idlnegcl  38001  divrngidl  38007  intidl  38008  unichnidl  38010  keridl  38011  igenmin  38043  prnc  38046  ispridlc  38049  erimeq2  38655  prter3  38860  glbconxN  39357  atltcvr  39414  3dim1  39446  lvolnle3at  39561  linepsubN  39731  osumclN  39946  pexmidALTN  39957  lhpmatb  40010  cdlemg1idlemN  40551  dihlss  41229  dihglblem5aN  41271  dihatlat  41313  aks6d1c1p1  42080  aks6d1c5lem1  42109  unitscyglem4  42171  f1o2d2  42206  pwsgprod  42517  selvvvval  42558  fsuppind  42563  fsuppssindlem1  42564  prjspertr  42578  prjspreln0  42582  lsmfgcl  43047  kercvrlsm  43056  unxpwdom3  43068  hbt  43103  oa0suclim  43248  om0suclim  43249  oe0suclim  43250  naddcnff  43335  cvgdvgrat  44286  climinf  45588  clim2f  45618  clim2cf  45632  clim0cf  45636  clim2f2  45652  fmtnofac2lem  47553  ovmpordxf  48324  oppcthinendcALT  49427  cotsqcscsq  49748  aacllem  49787