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  8097  infunsdom  10215  creui  12237  qreccl  13019  fsumrlim  15898  fsumo1  15899  climfsum  15907  imasvscaf  17625  grppropd  19075  grpinvpropd  19138  cycsubgcl  19334  frgpup1  19902  ringrghm  20455  phlpropd  21868  mamuass  22624  iccpnfcnv  25172  mbfeqalem1  25869  mbfinf  25893  mbflimsup  25894  mbflimlem  25895  itgfsum  26054  plypf1  26438  mtest  26640  rpvmasum2  27748  ifeqeqx  33017  ordtconnlem1  34434  xrge0iifcnv  34443  fsum2dsub  35115  regsfromregtco  37157  fvineqsneu  38165  pibt2  38171  incsequz  38498  equivtotbnd  38528  intidl  38779  keridl  38782  prnc  38817  cdleme50trn123  41427  dva1dim  41858  dia1dim2  41935  3factsumint1  42887  modelac8prim  45815