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  6179  1stconst  8098  infunsdom  10218  creui  12240  qreccl  13022  fsumrlim  15901  fsumo1  15902  climfsum  15910  imasvscaf  17628  grppropd  19078  grpinvpropd  19141  cycsubgcl  19337  frgpup1  19905  ringrghm  20458  phlpropd  21871  mamuass  22627  iccpnfcnv  25175  mbfeqalem1  25872  mbfinf  25896  mbflimsup  25897  mbflimlem  25898  itgfsum  26057  plypf1  26441  mtest  26643  rpvmasum2  27751  ifeqeqx  33020  ordtconnlem1  34437  xrge0iifcnv  34446  fsum2dsub  35118  regsfromregtco  37160  fvineqsneu  38168  pibt2  38174  incsequz  38501  equivtotbnd  38531  intidl  38782  keridl  38785  prnc  38820  cdleme50trn123  41430  dva1dim  41861  dia1dim2  41938  3factsumint1  42890  modelac8prim  45818