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  6177  1stconst  8114  infunsdom  10295  creui  12319  qreccl  13101  fsumrlim  15984  fsumo1  15985  climfsum  15993  imasvscaf  17717  grppropd  19168  grpinvpropd  19231  cycsubgcl  19427  frgpup1  19995  ringrghm  20550  phlpropd  21967  mamuass  22723  iccpnfcnv  25271  mbfeqalem1  25968  mbfinf  25992  mbflimsup  25993  mbflimlem  25994  itgfsum  26153  plypf1  26537  mtest  26737  rpvmasum2  27845  ifeqeqx  33186  ordtconnlem1  34603  xrge0iifcnv  34612  fsum2dsub  35283  regsfromregtco  37419  fvineqsneu  38428  pibt2  38434  incsequz  38776  equivtotbnd  38806  intidl  39057  keridl  39060  prnc  39095  cdleme50trn123  41705  dva1dim  42136  dia1dim2  42213  3factsumint1  43165  modelac8prim  46076