Theorem anassrs 404

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 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  anass  405  mpanr1  441  anass1rs  577  anabss5  584  anabss7  589  2ralbida  2571  2rexbidva  2573  ralimdvva  2619  pofun  4457  issod  4464  imainss  5203  fvelimab  5759  eqfnfv2  5807  funconstss  5827  fnex  5937  rexima  5960  ralima  5961  f1elima  5979  fliftfun  6002  isores2  6019  isosolem  6030  f1oiso  6032  ovmpodxf  6214  tfrlemibxssdm  6598  oav2  6736  omv2  6738  nnaass  6758  eroveu  6900  prarloclem4  7865  genpml  7884  genpmu  7885  genpassl  7891  genpassu  7892  prmuloc2  7934  addcomprg  7945  mulcomprg  7947  ltaddpr  7964  ltexprlemloc  7974  addcanprlemu  7982  recexgt0sr  8140  reapmul1  8924  apreim  8932  recexaplem2  8981  creur  9290  uz11  9947  xaddass  10273  xleadd1a  10277  xlt2add  10284  fzrevral  10514  seq3caopr2  10932  seqcaopr2g  10933  expnlbnd2  11105  shftlem  11583  resqrexlemgt0  11788  cau3lem  11882  clim2  12051  clim2c  12052  clim0c  12054  2clim  12069  climabs0  12075  climcn1  12076  climcn2  12077  climsqz  12103  climsqz2  12104  summodclem2  12151  fsum2dlemstep  12203  fsumiun  12246  mertenslem2  12305  mertensabs  12306  prodfrecap  12315  fprodeq0  12386  fprod2dlemstep  12391  gcdmultiplez  12800  dvdssq  12810  lcmgcdlem  12857  lcmdvds  12859  coprmdvds2  12873  pclemub  13068  pcxqcl  13093  pcge0  13094  pcgcd1  13109  prmpwdvds  13136  1arithlem4  13147  4sqlem18  13189  imasaddfnlemg  13637  imasaddflemg  13639  grpidpropdg  13696  grprida  13709  mhmpropd  13775  mhmima  13800  grplcan  13869  dfgrp3mlem  13905  mulgdirlem  13958  subgmulg  13993  issubg4m  13998  subgintm  14003  ssnmz  14016  rngpropd  14256  srglmhm  14299  srgrmhm  14300  ringpropd  14345  ringlghm  14368  dvdsrpropdg  14456  isnzr2  14493  islmod  14629  islmodd  14631  lmodprop2d  14687  lsssubg  14716  lsspropdg  14770  lidlsubg  14825  expghmap  14944  assapropd  15016  asclpropd  15042  neipsm  15257  lmbrf  15318  lmss  15349  txbas  15361  txbasval  15370  tx1cn  15372  txlm  15382  isxmet2d  15451  elmopn2  15552  mopni3  15587  blsscls2  15596  metequiv2  15599  metss2lem  15600  metrest  15609  metcnp  15615  metcnp2  15616  metcnpi3  15620  elcncf2  15677  mulc1cncf  15692  cncfco  15694  cncfmet  15695  fsumdvdsmul  16111  2sqlem9  16255