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  2552  2rexbidva  2554  ralimdvva  2600  pofun  4411  issod  4418  imainss  5154  fvelimab  5705  eqfnfv2  5748  funconstss  5768  fnex  5879  rexima  5900  ralima  5901  f1elima  5919  fliftfun  5942  isores2  5959  isosolem  5970  f1oiso  5972  ovmpodxf  6152  tfrlemibxssdm  6498  oav2  6636  omv2  6638  nnaass  6658  eroveu  6800  prarloclem4  7723  genpml  7742  genpmu  7743  genpassl  7749  genpassu  7750  prmuloc2  7792  addcomprg  7803  mulcomprg  7805  ltaddpr  7822  ltexprlemloc  7832  addcanprlemu  7840  recexgt0sr  7998  reapmul1  8780  apreim  8788  recexaplem2  8837  creur  9144  uz11  9784  xaddass  10109  xleadd1a  10113  xlt2add  10120  fzrevral  10345  seq3caopr2  10761  seqcaopr2g  10762  expnlbnd2  10933  shftlem  11399  resqrexlemgt0  11603  cau3lem  11697  clim2  11866  clim2c  11867  clim0c  11869  2clim  11884  climabs0  11890  climcn1  11891  climcn2  11892  climsqz  11918  climsqz2  11919  summodclem2  11966  fsum2dlemstep  12018  fsumiun  12061  mertenslem2  12120  mertensabs  12121  prodfrecap  12130  fprodeq0  12201  fprod2dlemstep  12206  gcdmultiplez  12615  dvdssq  12625  lcmgcdlem  12672  lcmdvds  12674  coprmdvds2  12688  pclemub  12883  pcxqcl  12908  pcge0  12909  pcgcd1  12924  prmpwdvds  12951  1arithlem4  12962  4sqlem18  13004  imasaddfnlemg  13420  imasaddflemg  13422  grpidpropdg  13480  grprida  13493  gsumpropd2  13499  mhmpropd  13572  mhmima  13597  grplcan  13668  dfgrp3mlem  13704  mulgdirlem  13763  subgmulg  13798  issubg4m  13803  subgintm  13808  ssnmz  13821  rngpropd  13992  srglmhm  14030  srgrmhm  14031  ringpropd  14075  ringlghm  14098  dvdsrpropdg  14185  isnzr2  14222  islmod  14329  islmodd  14331  lmodprop2d  14386  lsssubg  14415  lsspropdg  14469  lidlsubg  14524  expghmap  14645  neipsm  14907  lmbrf  14968  lmss  14999  txbas  15011  txbasval  15020  tx1cn  15022  txlm  15032  isxmet2d  15101  elmopn2  15202  mopni3  15237  blsscls2  15246  metequiv2  15249  metss2lem  15250  metrest  15259  metcnp  15265  metcnp2  15266  metcnpi3  15270  elcncf2  15327  mulc1cncf  15342  cncfco  15344  cncfmet  15345  fsumdvdsmul  15744  2sqlem9  15882