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  7584  genpml  7603  genpmu  7604  genpassl  7610  genpassu  7611  prmuloc2  7653  addcomprg  7664  mulcomprg  7666  ltaddpr  7683  ltexprlemloc  7693  addcanprlemu  7701  recexgt0sr  7859  reapmul1  8641  apreim  8649  recexaplem2  8698  creur  9005  uz11  9643  xaddass  9963  xleadd1a  9967  xlt2add  9974  fzrevral  10199  seq3caopr2  10604  seqcaopr2g  10605  expnlbnd2  10776  shftlem  11000  resqrexlemgt0  11204  cau3lem  11298  clim2  11467  clim2c  11468  clim0c  11470  2clim  11485  climabs0  11491  climcn1  11492  climcn2  11493  climsqz  11519  climsqz2  11520  summodclem2  11566  fsum2dlemstep  11618  fsumiun  11661  mertenslem2  11720  mertensabs  11721  prodfrecap  11730  fprodeq0  11801  fprod2dlemstep  11806  gcdmultiplez  12215  dvdssq  12225  lcmgcdlem  12272  lcmdvds  12274  coprmdvds2  12288  pclemub  12483  pcxqcl  12508  pcge0  12509  pcgcd1  12524  prmpwdvds  12551  1arithlem4  12562  4sqlem18  12604  imasaddfnlemg  13018  imasaddflemg  13020  grpidpropdg  13078  grprida  13091  gsumpropd2  13097  mhmpropd  13170  mhmima  13195  grplcan  13266  dfgrp3mlem  13302  mulgdirlem  13361  subgmulg  13396  issubg4m  13401  subgintm  13406  ssnmz  13419  rngpropd  13589  srglmhm  13627  srgrmhm  13628  ringpropd  13672  ringlghm  13695  dvdsrpropdg  13781  isnzr2  13818  islmod  13925  islmodd  13927  lmodprop2d  13982  lsssubg  14011  lsspropdg  14065  lidlsubg  14120  expghmap  14241  neipsm  14498  lmbrf  14559  lmss  14590  txbas  14602  txbasval  14611  tx1cn  14613  txlm  14623  isxmet2d  14692  elmopn2  14793  mopni3  14828  blsscls2  14837  metequiv2  14840  metss2lem  14841  metrest  14850  metcnp  14856  metcnp2  14857  metcnpi3  14861  elcncf2  14918  mulc1cncf  14933  cncfco  14935  cncfmet  14936  fsumdvdsmul  15335  2sqlem9  15473