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  2551  2rexbidva  2553  ralimdvva  2599  pofun  4404  issod  4411  imainss  5147  fvelimab  5695  eqfnfv2  5738  funconstss  5758  fnex  5868  rexima  5887  ralima  5888  f1elima  5906  fliftfun  5929  isores2  5946  isosolem  5957  f1oiso  5959  ovmpodxf  6139  tfrlemibxssdm  6484  oav2  6622  omv2  6624  nnaass  6644  eroveu  6786  prarloclem4  7701  genpml  7720  genpmu  7721  genpassl  7727  genpassu  7728  prmuloc2  7770  addcomprg  7781  mulcomprg  7783  ltaddpr  7800  ltexprlemloc  7810  addcanprlemu  7818  recexgt0sr  7976  reapmul1  8758  apreim  8766  recexaplem2  8815  creur  9122  uz11  9762  xaddass  10082  xleadd1a  10086  xlt2add  10093  fzrevral  10318  seq3caopr2  10732  seqcaopr2g  10733  expnlbnd2  10904  shftlem  11348  resqrexlemgt0  11552  cau3lem  11646  clim2  11815  clim2c  11816  clim0c  11818  2clim  11833  climabs0  11839  climcn1  11840  climcn2  11841  climsqz  11867  climsqz2  11868  summodclem2  11914  fsum2dlemstep  11966  fsumiun  12009  mertenslem2  12068  mertensabs  12069  prodfrecap  12078  fprodeq0  12149  fprod2dlemstep  12154  gcdmultiplez  12563  dvdssq  12573  lcmgcdlem  12620  lcmdvds  12622  coprmdvds2  12636  pclemub  12831  pcxqcl  12856  pcge0  12857  pcgcd1  12872  prmpwdvds  12899  1arithlem4  12910  4sqlem18  12952  imasaddfnlemg  13368  imasaddflemg  13370  grpidpropdg  13428  grprida  13441  gsumpropd2  13447  mhmpropd  13520  mhmima  13545  grplcan  13616  dfgrp3mlem  13652  mulgdirlem  13711  subgmulg  13746  issubg4m  13751  subgintm  13756  ssnmz  13769  rngpropd  13939  srglmhm  13977  srgrmhm  13978  ringpropd  14022  ringlghm  14045  dvdsrpropdg  14132  isnzr2  14169  islmod  14276  islmodd  14278  lmodprop2d  14333  lsssubg  14362  lsspropdg  14416  lidlsubg  14471  expghmap  14592  neipsm  14849  lmbrf  14910  lmss  14941  txbas  14953  txbasval  14962  tx1cn  14964  txlm  14974  isxmet2d  15043  elmopn2  15144  mopni3  15179  blsscls2  15188  metequiv2  15191  metss2lem  15192  metrest  15201  metcnp  15207  metcnp2  15208  metcnpi3  15212  elcncf2  15269  mulc1cncf  15284  cncfco  15286  cncfmet  15287  fsumdvdsmul  15686  2sqlem9  15824