Theorem anass1rs 668

Description: Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis

Ref	Expression
anass1rs.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
anass1rs	⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Proof of Theorem anass1rs

Step	Hyp	Ref	Expression
1		anass1rs.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	anassrs 473	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	an32s 665	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sossfld  6178  1stconst  8109  infunsdom  10284  creui  12308  qreccl  13090  fsumrlim  15971  fsumo1  15972  climfsum  15980  imasvscaf  17704  grppropd  19155  grpinvpropd  19218  cycsubgcl  19414  frgpup1  19982  ringrghm  20537  phlpropd  21954  mamuass  22710  iccpnfcnv  25258  mbfeqalem1  25955  mbfinf  25979  mbflimsup  25980  mbflimlem  25981  itgfsum  26140  plypf1  26524  mtest  26724  rpvmasum2  27832  ifeqeqx  33131  ordtconnlem1  34549  xrge0iifcnv  34558  fsum2dsub  35229  regsfromregtco  37306  fvineqsneu  38314  pibt2  38320  incsequz  38662  equivtotbnd  38692  intidl  38943  keridl  38946  prnc  38981  cdleme50trn123  41591  dva1dim  42022  dia1dim2  42099  3factsumint1  43051  modelac8prim  45960