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  2531  2rexbidva  2533  ralimdvva  2579  pofun  4380  issod  4387  imainss  5120  fvelimab  5663  eqfnfv2  5706  funconstss  5726  fnex  5834  rexima  5851  ralima  5852  f1elima  5870  fliftfun  5893  isores2  5910  isosolem  5921  f1oiso  5923  ovmpodxf  6101  tfrlemibxssdm  6443  oav2  6579  omv2  6581  nnaass  6601  eroveu  6743  prarloclem4  7653  genpml  7672  genpmu  7673  genpassl  7679  genpassu  7680  prmuloc2  7722  addcomprg  7733  mulcomprg  7735  ltaddpr  7752  ltexprlemloc  7762  addcanprlemu  7770  recexgt0sr  7928  reapmul1  8710  apreim  8718  recexaplem2  8767  creur  9074  uz11  9713  xaddass  10033  xleadd1a  10037  xlt2add  10044  fzrevral  10269  seq3caopr2  10682  seqcaopr2g  10683  expnlbnd2  10854  shftlem  11293  resqrexlemgt0  11497  cau3lem  11591  clim2  11760  clim2c  11761  clim0c  11763  2clim  11778  climabs0  11784  climcn1  11785  climcn2  11786  climsqz  11812  climsqz2  11813  summodclem2  11859  fsum2dlemstep  11911  fsumiun  11954  mertenslem2  12013  mertensabs  12014  prodfrecap  12023  fprodeq0  12094  fprod2dlemstep  12099  gcdmultiplez  12508  dvdssq  12518  lcmgcdlem  12565  lcmdvds  12567  coprmdvds2  12581  pclemub  12776  pcxqcl  12801  pcge0  12802  pcgcd1  12817  prmpwdvds  12844  1arithlem4  12855  4sqlem18  12897  imasaddfnlemg  13313  imasaddflemg  13315  grpidpropdg  13373  grprida  13386  gsumpropd2  13392  mhmpropd  13465  mhmima  13490  grplcan  13561  dfgrp3mlem  13597  mulgdirlem  13656  subgmulg  13691  issubg4m  13696  subgintm  13701  ssnmz  13714  rngpropd  13884  srglmhm  13922  srgrmhm  13923  ringpropd  13967  ringlghm  13990  dvdsrpropdg  14076  isnzr2  14113  islmod  14220  islmodd  14222  lmodprop2d  14277  lsssubg  14306  lsspropdg  14360  lidlsubg  14415  expghmap  14536  neipsm  14793  lmbrf  14854  lmss  14885  txbas  14897  txbasval  14906  tx1cn  14908  txlm  14918  isxmet2d  14987  elmopn2  15088  mopni3  15123  blsscls2  15132  metequiv2  15135  metss2lem  15136  metrest  15145  metcnp  15151  metcnp2  15152  metcnpi3  15156  elcncf2  15213  mulc1cncf  15228  cncfco  15230  cncfmet  15231  fsumdvdsmul  15630  2sqlem9  15768