Theorem anassrs 398

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 363	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 254	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  anass  399  mpanr1  434  anass1rs  561  anabss5  568  anabss7  573  2ralbida  2485  2rexbidva  2487  ralimdvva  2533  pofun  4284  issod  4291  imainss  5013  fvelimab  5536  eqfnfv2  5578  funconstss  5597  fnex  5701  rexima  5717  ralima  5718  f1elima  5735  fliftfun  5758  isores2  5775  isosolem  5786  f1oiso  5788  ovmpodxf  5958  grpridd  6029  tfrlemibxssdm  6286  oav2  6422  omv2  6424  nnaass  6444  eroveu  6583  prarloclem4  7430  genpml  7449  genpmu  7450  genpassl  7456  genpassu  7457  prmuloc2  7499  addcomprg  7510  mulcomprg  7512  ltaddpr  7529  ltexprlemloc  7539  addcanprlemu  7547  recexgt0sr  7705  reapmul1  8484  apreim  8492  recexaplem2  8540  creur  8845  uz11  9479  xaddass  9796  xleadd1a  9800  xlt2add  9807  fzrevral  10030  seq3caopr2  10407  expnlbnd2  10569  shftlem  10744  resqrexlemgt0  10948  cau3lem  11042  clim2  11210  clim2c  11211  clim0c  11213  2clim  11228  climabs0  11234  climcn1  11235  climcn2  11236  climsqz  11262  climsqz2  11263  summodclem2  11309  fsum2dlemstep  11361  fsumiun  11404  mertenslem2  11463  mertensabs  11464  prodfrecap  11473  fprodeq0  11544  fprod2dlemstep  11549  gcdmultiplez  11939  dvdssq  11949  lcmgcdlem  11988  lcmdvds  11990  coprmdvds2  12004  pclemub  12196  pcge0  12221  pcgcd1  12236  neipsm  12695  lmbrf  12756  lmss  12787  txbas  12799  txbasval  12808  tx1cn  12810  txlm  12820  isxmet2d  12889  elmopn2  12990  mopni3  13025  blsscls2  13034  metequiv2  13037  metss2lem  13038  metrest  13047  metcnp  13053  metcnp2  13054  metcnpi3  13058  elcncf2  13102  mulc1cncf  13117  cncfco  13119  cncfmet  13120