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  2528  2rexbidva  2530  ralimdvva  2576  pofun  4363  issod  4370  imainss  5103  fvelimab  5642  eqfnfv2  5685  funconstss  5705  fnex  5813  rexima  5830  ralima  5831  f1elima  5849  fliftfun  5872  isores2  5889  isosolem  5900  f1oiso  5902  ovmpodxf  6078  tfrlemibxssdm  6420  oav2  6556  omv2  6558  nnaass  6578  eroveu  6720  prarloclem4  7618  genpml  7637  genpmu  7638  genpassl  7644  genpassu  7645  prmuloc2  7687  addcomprg  7698  mulcomprg  7700  ltaddpr  7717  ltexprlemloc  7727  addcanprlemu  7735  recexgt0sr  7893  reapmul1  8675  apreim  8683  recexaplem2  8732  creur  9039  uz11  9678  xaddass  9998  xleadd1a  10002  xlt2add  10009  fzrevral  10234  seq3caopr2  10645  seqcaopr2g  10646  expnlbnd2  10817  shftlem  11171  resqrexlemgt0  11375  cau3lem  11469  clim2  11638  clim2c  11639  clim0c  11641  2clim  11656  climabs0  11662  climcn1  11663  climcn2  11664  climsqz  11690  climsqz2  11691  summodclem2  11737  fsum2dlemstep  11789  fsumiun  11832  mertenslem2  11891  mertensabs  11892  prodfrecap  11901  fprodeq0  11972  fprod2dlemstep  11977  gcdmultiplez  12386  dvdssq  12396  lcmgcdlem  12443  lcmdvds  12445  coprmdvds2  12459  pclemub  12654  pcxqcl  12679  pcge0  12680  pcgcd1  12695  prmpwdvds  12722  1arithlem4  12733  4sqlem18  12775  imasaddfnlemg  13190  imasaddflemg  13192  grpidpropdg  13250  grprida  13263  gsumpropd2  13269  mhmpropd  13342  mhmima  13367  grplcan  13438  dfgrp3mlem  13474  mulgdirlem  13533  subgmulg  13568  issubg4m  13573  subgintm  13578  ssnmz  13591  rngpropd  13761  srglmhm  13799  srgrmhm  13800  ringpropd  13844  ringlghm  13867  dvdsrpropdg  13953  isnzr2  13990  islmod  14097  islmodd  14099  lmodprop2d  14154  lsssubg  14183  lsspropdg  14237  lidlsubg  14292  expghmap  14413  neipsm  14670  lmbrf  14731  lmss  14762  txbas  14774  txbasval  14783  tx1cn  14785  txlm  14795  isxmet2d  14864  elmopn2  14965  mopni3  15000  blsscls2  15009  metequiv2  15012  metss2lem  15013  metrest  15022  metcnp  15028  metcnp2  15029  metcnpi3  15033  elcncf2  15090  mulc1cncf  15105  cncfco  15107  cncfmet  15108  fsumdvdsmul  15507  2sqlem9  15645