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

This theorem is referenced by:  anass  469  anass1rs  652  anabss5  665  anabss7  670  mpanr1  700  pm2.61ddan  811  pm2.61dda  812  pm2.61da2ne  3034  ralimdvva  3127  2ralbidva  3129  2ralbida  3163  reximdvva  3207  2rexbidva  3229  copsexgw  5405  copsexg  5406  pofun  5522  imainss  6062  fvmptdf  6890  eqfnfv2  6919  fnex  7102  f1elima  7145  fliftfun  7192  isores2  7213  f1oiso  7231  ovmpodxf  7432  sorpssuni  7594  sorpssint  7595  tfindsg2  7717  2ndconst  7950  oalim  8371  omlim  8372  oaass  8401  omlimcl  8418  omass  8420  oelim2  8435  oeoa  8437  oeoelem  8438  nnaass  8462  omabs  8490  eroveu  8610  sbthlem4  8882  fimaxg  9070  fisupg  9071  fofinf1o  9103  fiming  9266  fiinfg  9267  ordtypelem7  9292  hartogs  9312  card2on  9322  unwdomg  9352  wemapwe  9464  frmin  9516  dfac5  9893  cfsmolem  10035  isf32lem2  10119  ttukeylem6  10279  ondomon  10328  alephreg  10347  ltexprlem6  10806  recexsrlem  10868  wloglei  11516  recextlem2  11615  fimaxre  11928  creur  11976  uz11  12616  xrmaxeq  12922  xrmineq  12923  xaddf  12967  xaddass  12992  xleadd1a  12996  xlt2add  13003  xmullem  13007  xmulgt0  13026  xmulasslem3  13029  xlemul1a  13031  xadddilem  13037  fzrevral  13350  seqcaopr2  13768  expnlbnd2  13958  faclbnd4lem4  14019  hashgt23el  14148  rtrclreclem3  14780  rtrclreclem4  14781  relexpindlem  14783  rtrclind  14785  shftlem  14788  01sqrex  14970  cau3lem  15075  limsupbnd2  15201  clim2  15222  clim2c  15223  clim0c  15225  rlimresb  15283  2clim  15290  climabs0  15303  climcn1  15310  climcn2  15311  o1rlimmul  15337  climsqz  15359  climsqz2  15360  rlimsqzlem  15369  lo1le  15372  climsup  15390  caucvgrlem2  15395  iseralt  15405  summolem2  15437  fsum2dlem  15491  cvgcmp  15537  cvgcmpce  15539  climfsum  15541  fsumiun  15542  geomulcvg  15597  mertenslem2  15606  mertens  15607  prodfn0  15615  prodfrec  15616  zprod  15656  fprodeq0  15694  fprodn0  15698  fprod2dlem  15699  smu01lem  16201  gcdcllem1  16215  gcdmultiplezOLD  16270  dvdssq  16281  lcmdvds  16322  coprmdvds2  16368  pclem  16548  pcge0  16572  pcgcd1  16587  prmpwdvds  16614  1arithlem4  16636  4sqlem18  16672  vdwlem10  16700  vdwlem11  16701  ramval  16718  ramub1lem2  16737  ramcl  16739  imasaddfnlem  17248  imasaddflem  17250  imasvscafn  17257  imasleval  17261  ismon2  17455  isepi2  17462  issubc3  17573  cofucl  17612  setcmon  17811  setcepi  17812  ipodrsfi  18266  ipodrsima  18268  isacs3lem  18269  grpidpropd  18355  grpridd  18368  gsumpropd2lem  18372  mhmpropd  18445  mhmima  18472  gsumccatOLD  18488  grplcan  18646  dfgrp3lem  18682  mulgdirlem  18743  subgmulg  18778  issubg4  18783  subgint  18788  ssnmz  18803  cycsubgcl  18834  gastacl  18924  orbsta  18928  cntzsubg  18952  galactghm  19021  odmulg  19172  odbezout  19174  sylow3lem2  19242  lsmsubm  19267  efgsfo  19354  mulgmhm  19438  mulgghm  19439  gsumval3  19517  gsumcllem  19518  gsumpt  19572  gsum2d  19582  gsum2d2  19584  prdsgsum  19591  subgdmdprd  19646  dprd2d2  19656  ablfac1eu  19685  srglmhm  19780  srgrmhm  19781  ringpropd  19830  ringlghm  19852  dvdsrpropd  19947  cntzsdrg  20079  abvpropd  20111  islmodd  20138  lmodprop2d  20194  lsssubg  20228  lsspropd  20288  lmhmima  20318  lidlsubg  20495  phlpropd  20869  frlmsslsp  21012  lindfmm  21043  islindf4  21054  assapropd  21085  asclpropd  21110  psrass1lemOLD  21152  psrass1lem  21155  mplcoe1  21247  mplcoe5  21250  mplind  21287  evlslem2  21298  evlsval  21305  coe1tmmul2  21456  mamuass  21558  mavmulass  21707  mdetuni0  21779  mdetmul  21781  cpmatacl  21874  cpmadugsumfi  22035  cpmadumatpolylem1  22039  cpmadumatpolylem2  22040  cpmadumatpoly  22041  cayhamlem4  22046  neips  22273  neindisj  22277  ordtrest2lem  22363  lmbrf  22420  lmss  22458  isreg2  22537  lmmo  22540  hauscmplem  22566  bwth  22570  2ndcomap  22618  1stcelcls  22621  restlly  22643  islly2  22644  cldllycmp  22655  comppfsc  22692  1stckgenlem  22713  txbas  22727  txbasval  22766  tx1cn  22769  ptpjopn  22772  ptcnp  22782  txnlly  22797  txlm  22808  xkococn  22820  fgabs  23039  fmfnfmlem4  23117  flimcf  23142  hauspwpwf1  23147  fclsbas  23181  fclscf  23185  flimfnfcls  23188  ghmcnp  23275  tsmsxp  23315  isxmet2d  23489  elmopn2  23607  mopni3  23659  blsscls2  23669  metequiv2  23675  metss2lem  23676  met2ndci  23687  metrest  23689  metcnp  23706  metcnp2  23707  metcnpi3  23711  txmetcnp  23712  nmolb2d  23891  xrge0tsms  24006  metdsre  24025  metnrmlem3  24033  fsumcn  24042  elcncf2  24062  mulc1cncf  24077  cncfco  24079  cncfmet  24081  bndth  24130  evth  24131  copco  24190  pcopt2  24195  pcoass  24196  pcorevlem  24198  lmmcvg  24434  lmmbrf  24435  iscau4  24452  iscauf  24453  cmetcaulem  24461  iscmet3lem3  24463  iscmet3lem1  24464  causs  24471  equivcfil  24472  lmclim  24476  caubl  24481  caublcls  24482  bcth3  24504  ivthle  24629  ivthle2  24630  ovoliunlem1  24675  ovolicc2lem5  24694  volsuplem  24728  uniioombllem6  24761  dyaddisjlem  24768  dyadmax  24771  volcn  24779  mbfmulc2lem  24820  ismbf3d  24827  mbfsup  24837  mbfinf  24838  mbflim  24841  i1fmullem  24867  itg2seq  24916  itg2uba  24917  itg2splitlem  24922  itg2split  24923  itg2monolem1  24924  bddiblnc  25015  ditgsplitlem  25033  ellimc2  25050  ellimc3  25052  limcflf  25054  limcmpt  25056  limcco  25066  lhop1lem  25186  dvfsumle  25194  dvfsumabs  25196  dvfsumrlim  25204  ftc1a  25210  ftc1lem6  25214  mdegmullem  25252  elply2  25366  plypf1  25382  ulmcaulem  25562  ulmcau  25563  ulmss  25565  ulmdvlem3  25570  mtest  25572  itgulm  25576  abelthlem8  25607  abelth  25609  tanord  25703  cxpcn3lem  25909  mcubic  26006  cubic2  26007  dvdsflsumcom  26346  fsumdvdsmul  26353  lgsdchrval  26511  2sqlem9  26584  rplogsumlem2  26642  rpvmasumlem  26644  dchrvmasumlem1  26652  vmalogdivsum2  26695  logsqvma  26699  selberg  26705  selberg4  26718  pntibndlem3  26749  pntlem3  26766  pntleml  26768  padicabv  26787  padicabvf  26788  padicabvcxp  26789  ostth3  26795  axpasch  27318  axcontlem7  27347  axcontlem10  27350  cusgrsize2inds  27829  grpolcan  28901  nvmul0or  29021  nmosetre  29135  blocnilem  29175  blocni  29176  h2hcau  29350  h2hlm  29351  shsel3  29686  chscllem2  30009  homulcl  30130  adjsym  30204  cnvadj  30263  hhcno  30275  hhcnf  30276  lnopl  30285  unoplin  30291  counop  30292  lnfnl  30302  hmoplin  30313  hmopm  30392  nmcexi  30397  lnconi  30404  riesz3i  30433  leopmuli  30504  leopmul  30505  hstle  30601  mdsl0  30681  mdslmd1lem2  30697  atcvatlem  30756  chirredi  30765  cdj1i  30804  sbc2iedf  30824  foresf1o  30859  suppovss  31026  isoun  31043  difioo  31112  swrdf1  31237  xrge0tsmsd  31326  cycpmrn  31419  fedgmullem2  31720  pstmxmet  31856  ordtrest2NEWlem  31881  esum2dlem  32069  esum2d  32070  dya2icoseg2  32254  eulerpartlemgc  32338  eulerpartlemgh  32354  eulerpartlemgs2  32356  ballotlemimin  32481  signstfvneq0  32560  hgt750lemb  32645  connpconn  33206  cvmliftmolem2  33253  cvmliftlem6  33261  cvmliftlem8  33263  cvmlift2lem12  33285  elmrsubrn  33491  dfon2lem6  33773  poxp2  33799  xpord3pred  33807  sexp3  33808  poseq  33811  nosupbnd1lem5  33924  noinfbnd1lem5  33939  nocvxminlem  33981  lrrecfr  34109  ifscgr  34355  brsegle  34419  neibastop2lem  34558  bj-elabd2ALT  35122  bj-ismooredr2  35290  curf  35764  finixpnum  35771  fin2solem  35772  fin2so  35773  lindsenlbs  35781  matunitlindflem1  35782  matunitlindflem2  35783  matunitlindf  35784  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem14  35800  poimirlem16  35802  poimirlem19  35805  poimirlem22  35808  poimirlem28  35814  poimirlem29  35815  poimirlem30  35816  poimir  35819  heicant  35821  itg2gt0cn  35841  ftc1cnnc  35858  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anc  35867  cover2  35881  filbcmb  35907  fdc  35912  fdc1  35913  seqpo  35914  incsequz  35915  incsequz2  35916  metf1o  35922  lmclim2  35925  geomcau  35926  isbnd2  35950  bndss  35953  ismtybndlem  35973  heibor1lem  35976  rrncmslem  35999  rrnequiv  36002  exidreslem  36044  ghomco  36058  isdrngo3  36126  rngoisocnv  36148  isidlc  36182  idlnegcl  36189  divrngidl  36195  intidl  36196  unichnidl  36198  keridl  36199  igenmin  36231  prnc  36234  ispridlc  36237  erim2  36796  prter3  36903  glbconxN  37399  atltcvr  37456  3dim1  37488  lvolnle3at  37603  linepsubN  37773  osumclN  37988  pexmidALTN  37999  lhpmatb  38052  cdlemg1idlemN  38593  dihlss  39271  dihglblem5aN  39313  dihatlat  39355  metakunt1  40132  metakunt2  40133  pwsgprod  40276  fsuppind  40286  fsuppssindlem1  40287  prjspertr  40451  prjspreln0  40455  lsmfgcl  40906  kercvrlsm  40915  unxpwdom3  40927  hbt  40962  cvgdvgrat  41938  climinf  43154  clim2f  43184  clim2cf  43198  clim0cf  43202  clim2f2  43218  fmtnofac2lem  45031  isomuspgrlem2d  45294  mgmhmpropd  45350  mgmhmima  45367  ovmpordxf  45685  cotsqcscsq  46475  aacllem  46516