Theorem anassrs 400

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  anass  401  mpanr1  437  anass1rs  571  anabss5  578  anabss7  583  2ralbida  2551  2rexbidva  2553  ralimdvva  2599  pofun  4403  issod  4410  imainss  5144  fvelimab  5692  eqfnfv2  5735  funconstss  5755  fnex  5865  rexima  5884  ralima  5885  f1elima  5903  fliftfun  5926  isores2  5943  isosolem  5954  f1oiso  5956  ovmpodxf  6136  tfrlemibxssdm  6479  oav2  6617  omv2  6619  nnaass  6639  eroveu  6781  prarloclem4  7693  genpml  7712  genpmu  7713  genpassl  7719  genpassu  7720  prmuloc2  7762  addcomprg  7773  mulcomprg  7775  ltaddpr  7792  ltexprlemloc  7802  addcanprlemu  7810  recexgt0sr  7968  reapmul1  8750  apreim  8758  recexaplem2  8807  creur  9114  uz11  9753  xaddass  10073  xleadd1a  10077  xlt2add  10084  fzrevral  10309  seq3caopr2  10723  seqcaopr2g  10724  expnlbnd2  10895  shftlem  11335  resqrexlemgt0  11539  cau3lem  11633  clim2  11802  clim2c  11803  clim0c  11805  2clim  11820  climabs0  11826  climcn1  11827  climcn2  11828  climsqz  11854  climsqz2  11855  summodclem2  11901  fsum2dlemstep  11953  fsumiun  11996  mertenslem2  12055  mertensabs  12056  prodfrecap  12065  fprodeq0  12136  fprod2dlemstep  12141  gcdmultiplez  12550  dvdssq  12560  lcmgcdlem  12607  lcmdvds  12609  coprmdvds2  12623  pclemub  12818  pcxqcl  12843  pcge0  12844  pcgcd1  12859  prmpwdvds  12886  1arithlem4  12897  4sqlem18  12939  imasaddfnlemg  13355  imasaddflemg  13357  grpidpropdg  13415  grprida  13428  gsumpropd2  13434  mhmpropd  13507  mhmima  13532  grplcan  13603  dfgrp3mlem  13639  mulgdirlem  13698  subgmulg  13733  issubg4m  13738  subgintm  13743  ssnmz  13756  rngpropd  13926  srglmhm  13964  srgrmhm  13965  ringpropd  14009  ringlghm  14032  dvdsrpropdg  14119  isnzr2  14156  islmod  14263  islmodd  14265  lmodprop2d  14320  lsssubg  14349  lsspropdg  14403  lidlsubg  14458  expghmap  14579  neipsm  14836  lmbrf  14897  lmss  14928  txbas  14940  txbasval  14949  tx1cn  14951  txlm  14961  isxmet2d  15030  elmopn2  15131  mopni3  15166  blsscls2  15175  metequiv2  15178  metss2lem  15179  metrest  15188  metcnp  15194  metcnp2  15195  metcnpi3  15199  elcncf2  15256  mulc1cncf  15271  cncfco  15273  cncfmet  15274  fsumdvdsmul  15673  2sqlem9  15811