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  573  anabss5  580  anabss7  585  2ralbida  2553  2rexbidva  2555  ralimdvva  2601  pofun  4409  issod  4416  imainss  5152  fvelimab  5702  eqfnfv2  5745  funconstss  5765  fnex  5876  rexima  5895  ralima  5896  f1elima  5914  fliftfun  5937  isores2  5954  isosolem  5965  f1oiso  5967  ovmpodxf  6147  tfrlemibxssdm  6493  oav2  6631  omv2  6633  nnaass  6653  eroveu  6795  prarloclem4  7718  genpml  7737  genpmu  7738  genpassl  7744  genpassu  7745  prmuloc2  7787  addcomprg  7798  mulcomprg  7800  ltaddpr  7817  ltexprlemloc  7827  addcanprlemu  7835  recexgt0sr  7993  reapmul1  8775  apreim  8783  recexaplem2  8832  creur  9139  uz11  9779  xaddass  10104  xleadd1a  10108  xlt2add  10115  fzrevral  10340  seq3caopr2  10756  seqcaopr2g  10757  expnlbnd2  10928  shftlem  11378  resqrexlemgt0  11582  cau3lem  11676  clim2  11845  clim2c  11846  clim0c  11848  2clim  11863  climabs0  11869  climcn1  11870  climcn2  11871  climsqz  11897  climsqz2  11898  summodclem2  11945  fsum2dlemstep  11997  fsumiun  12040  mertenslem2  12099  mertensabs  12100  prodfrecap  12109  fprodeq0  12180  fprod2dlemstep  12185  gcdmultiplez  12594  dvdssq  12604  lcmgcdlem  12651  lcmdvds  12653  coprmdvds2  12667  pclemub  12862  pcxqcl  12887  pcge0  12888  pcgcd1  12903  prmpwdvds  12930  1arithlem4  12941  4sqlem18  12983  imasaddfnlemg  13399  imasaddflemg  13401  grpidpropdg  13459  grprida  13472  gsumpropd2  13478  mhmpropd  13551  mhmima  13576  grplcan  13647  dfgrp3mlem  13683  mulgdirlem  13742  subgmulg  13777  issubg4m  13782  subgintm  13787  ssnmz  13800  rngpropd  13971  srglmhm  14009  srgrmhm  14010  ringpropd  14054  ringlghm  14077  dvdsrpropdg  14164  isnzr2  14201  islmod  14308  islmodd  14310  lmodprop2d  14365  lsssubg  14394  lsspropdg  14448  lidlsubg  14503  expghmap  14624  neipsm  14881  lmbrf  14942  lmss  14973  txbas  14985  txbasval  14994  tx1cn  14996  txlm  15006  isxmet2d  15075  elmopn2  15176  mopni3  15211  blsscls2  15220  metequiv2  15223  metss2lem  15224  metrest  15233  metcnp  15239  metcnp2  15240  metcnpi3  15244  elcncf2  15301  mulc1cncf  15316  cncfco  15318  cncfmet  15319  fsumdvdsmul  15718  2sqlem9  15856