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  2518  2rexbidva  2520  ralimdvva  2566  pofun  4348  issod  4355  imainss  5086  fvelimab  5620  eqfnfv2  5663  funconstss  5683  fnex  5787  rexima  5804  ralima  5805  f1elima  5823  fliftfun  5846  isores2  5863  isosolem  5874  f1oiso  5876  ovmpodxf  6052  tfrlemibxssdm  6394  oav2  6530  omv2  6532  nnaass  6552  eroveu  6694  prarloclem4  7582  genpml  7601  genpmu  7602  genpassl  7608  genpassu  7609  prmuloc2  7651  addcomprg  7662  mulcomprg  7664  ltaddpr  7681  ltexprlemloc  7691  addcanprlemu  7699  recexgt0sr  7857  reapmul1  8639  apreim  8647  recexaplem2  8696  creur  9003  uz11  9641  xaddass  9961  xleadd1a  9965  xlt2add  9972  fzrevral  10197  seq3caopr2  10602  seqcaopr2g  10603  expnlbnd2  10774  shftlem  10998  resqrexlemgt0  11202  cau3lem  11296  clim2  11465  clim2c  11466  clim0c  11468  2clim  11483  climabs0  11489  climcn1  11490  climcn2  11491  climsqz  11517  climsqz2  11518  summodclem2  11564  fsum2dlemstep  11616  fsumiun  11659  mertenslem2  11718  mertensabs  11719  prodfrecap  11728  fprodeq0  11799  fprod2dlemstep  11804  gcdmultiplez  12213  dvdssq  12223  lcmgcdlem  12270  lcmdvds  12272  coprmdvds2  12286  pclemub  12481  pcxqcl  12506  pcge0  12507  pcgcd1  12522  prmpwdvds  12549  1arithlem4  12560  4sqlem18  12602  imasaddfnlemg  13016  imasaddflemg  13018  grpidpropdg  13076  grprida  13089  gsumpropd2  13095  mhmpropd  13168  mhmima  13193  grplcan  13264  dfgrp3mlem  13300  mulgdirlem  13359  subgmulg  13394  issubg4m  13399  subgintm  13404  ssnmz  13417  rngpropd  13587  srglmhm  13625  srgrmhm  13626  ringpropd  13670  ringlghm  13693  dvdsrpropdg  13779  isnzr2  13816  islmod  13923  islmodd  13925  lmodprop2d  13980  lsssubg  14009  lsspropdg  14063  lidlsubg  14118  expghmap  14239  neipsm  14474  lmbrf  14535  lmss  14566  txbas  14578  txbasval  14587  tx1cn  14589  txlm  14599  isxmet2d  14668  elmopn2  14769  mopni3  14804  blsscls2  14813  metequiv2  14816  metss2lem  14817  metrest  14826  metcnp  14832  metcnp2  14833  metcnpi3  14837  elcncf2  14894  mulc1cncf  14909  cncfco  14911  cncfmet  14912  fsumdvdsmul  15311  2sqlem9  15449