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  2563  2rexbidva  2565  ralimdvva  2611  pofun  4432  issod  4439  imainss  5177  fvelimab  5732  eqfnfv2  5775  funconstss  5795  fnex  5905  rexima  5926  ralima  5927  f1elima  5945  fliftfun  5968  isores2  5985  isosolem  5996  f1oiso  5998  ovmpodxf  6178  tfrlemibxssdm  6557  oav2  6695  omv2  6697  nnaass  6717  eroveu  6859  prarloclem4  7809  genpml  7828  genpmu  7829  genpassl  7835  genpassu  7836  prmuloc2  7878  addcomprg  7889  mulcomprg  7891  ltaddpr  7908  ltexprlemloc  7918  addcanprlemu  7926  recexgt0sr  8084  reapmul1  8865  apreim  8873  recexaplem2  8922  creur  9229  uz11  9873  xaddass  10198  xleadd1a  10202  xlt2add  10209  fzrevral  10435  seq3caopr2  10851  seqcaopr2g  10852  expnlbnd2  11023  shftlem  11494  resqrexlemgt0  11698  cau3lem  11792  clim2  11961  clim2c  11962  clim0c  11964  2clim  11979  climabs0  11985  climcn1  11986  climcn2  11987  climsqz  12013  climsqz2  12014  summodclem2  12061  fsum2dlemstep  12113  fsumiun  12156  mertenslem2  12215  mertensabs  12216  prodfrecap  12225  fprodeq0  12296  fprod2dlemstep  12301  gcdmultiplez  12710  dvdssq  12720  lcmgcdlem  12767  lcmdvds  12769  coprmdvds2  12783  pclemub  12978  pcxqcl  13003  pcge0  13004  pcgcd1  13019  prmpwdvds  13046  1arithlem4  13057  4sqlem18  13099  imasaddfnlemg  13516  imasaddflemg  13518  grpidpropdg  13576  grprida  13589  gsumpropd2  13595  mhmpropd  13668  mhmima  13693  grplcan  13764  dfgrp3mlem  13800  mulgdirlem  13859  subgmulg  13894  issubg4m  13899  subgintm  13904  ssnmz  13917  rngpropd  14088  srglmhm  14126  srgrmhm  14127  ringpropd  14171  ringlghm  14194  dvdsrpropdg  14281  isnzr2  14318  islmod  14426  islmodd  14428  lmodprop2d  14483  lsssubg  14512  lsspropdg  14566  lidlsubg  14621  expghmap  14742  neipsm  15006  lmbrf  15067  lmss  15098  txbas  15110  txbasval  15119  tx1cn  15121  txlm  15131  isxmet2d  15200  elmopn2  15301  mopni3  15336  blsscls2  15345  metequiv2  15348  metss2lem  15349  metrest  15358  metcnp  15364  metcnp2  15365  metcnpi3  15369  elcncf2  15426  mulc1cncf  15441  cncfco  15443  cncfmet  15444  fsumdvdsmul  15846  2sqlem9  15984