Theorem anassrs 404

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 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  anass  405  mpanr1  441  anass1rs  577  anabss5  584  anabss7  589  2ralbida  2571  2rexbidva  2573  ralimdvva  2619  pofun  4459  issod  4466  imainss  5206  fvelimab  5762  eqfnfv2  5810  funconstss  5830  fnex  5940  rexima  5963  ralima  5964  f1elima  5982  fliftfun  6005  isores2  6022  isosolem  6033  f1oiso  6035  ovmpodxf  6217  tfrlemibxssdm  6602  oav2  6740  omv2  6742  nnaass  6762  eroveu  6904  prarloclem4  7872  genpml  7891  genpmu  7892  genpassl  7898  genpassu  7899  prmuloc2  7941  addcomprg  7952  mulcomprg  7954  ltaddpr  7971  ltexprlemloc  7981  addcanprlemu  7989  recexgt0sr  8147  reapmul1  8932  apreim  8940  recexaplem2  8989  creur  9298  uz11  9962  xaddass  10289  xleadd1a  10293  xlt2add  10300  fzrevral  10530  seq3caopr2  10952  seqcaopr2g  10953  expnlbnd2  11125  shftlem  11604  resqrexlemgt0  11809  cau3lem  11904  clim2  12075  clim2c  12076  clim0c  12078  2clim  12093  climabs0  12099  climcn1  12100  climcn2  12101  climsqz  12127  climsqz2  12128  summodclem2  12175  fsum2dlemstep  12227  fsumiun  12270  mertenslem2  12329  mertensabs  12330  prodfrecap  12339  fprodeq0  12410  fprod2dlemstep  12415  gcdmultiplez  12824  dvdssq  12834  lcmgcdlem  12881  lcmdvds  12883  coprmdvds2  12897  pclemub  13096  pcxqcl  13121  pcge0  13122  pcgcd1  13137  prmpwdvds  13164  1arithlem4  13175  4sqlem18  13217  imasaddfnlemg  13695  imasaddflemg  13697  grpidpropdg  13754  grprida  13767  mhmpropd  13833  mhmima  13858  grplcan  13927  dfgrp3mlem  13963  mulgdirlem  14016  subgmulg  14051  issubg4m  14056  subgintm  14061  ssnmz  14074  cntzsubg  14172  gsum2d2fi  14275  rngpropd  14362  srglmhm  14405  srgrmhm  14406  ringpropd  14451  ringlghm  14474  dvdsrpropdg  14564  isnzr2  14601  islmod  14737  islmodd  14739  lmodprop2d  14795  lsssubg  14824  lsspropdg  14878  lidlsubg  14933  expghmap  15052  assapropd  15124  asclpropd  15150  psrass1filem  15182  neipsm  15392  lmbrf  15453  lmss  15484  txbas  15496  txbasval  15505  tx1cn  15507  txlm  15517  isxmet2d  15586  elmopn2  15687  mopni3  15722  blsscls2  15731  metequiv2  15734  metss2lem  15735  metrest  15744  metcnp  15750  metcnp2  15751  metcnpi3  15755  elcncf2  15812  mulc1cncf  15827  cncfco  15829  cncfmet  15830  zprmlogbaplem2  16228  fsumdvdsmul  16297  2sqlem9  16460