Theorem anass1rs 661

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 468	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	an32s 658	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  sossfld  6137  1stconst  8039  infunsdom  10126  creui  12145  qreccl  12910  fsumrlim  15765  fsumo1  15766  climfsum  15774  imasvscaf  17494  grppropd  18918  grpinvpropd  18982  cycsubgcl  19172  frgpup1  19741  ringrghm  20285  phlpropd  21630  mamuass  22385  iccpnfcnv  24929  mbfeqalem1  25626  mbfinf  25650  mbflimsup  25651  mbflimlem  25652  itgfsum  25812  plypf1  26195  mtest  26387  rpvmasum2  27493  ifeqeqx  32630  ordtconnlem1  34108  xrge0iifcnv  34117  fsum2dsub  34791  regsfromregtco  36766  fvineqsneu  37773  pibt2  37779  incsequz  38115  equivtotbnd  38145  intidl  38396  keridl  38399  prnc  38434  cdleme50trn123  41046  dva1dim  41477  dia1dim2  41554  3factsumint1  42506  modelac8prim  45436