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  6186  1stconst  8097  infunsdom  10208  creui  12224  qreccl  13005  fsumrlim  15882  fsumo1  15883  climfsum  15891  imasvscaf  17611  grppropd  19042  grpinvpropd  19105  cycsubgcl  19301  frgpup1  19869  ringrghm  20422  phlpropd  21835  mamuass  22589  iccpnfcnv  25134  mbfeqalem1  25831  mbfinf  25855  mbflimsup  25856  mbflimlem  25857  itgfsum  26017  plypf1  26400  mtest  26598  rpvmasum2  27707  ifeqeqx  32935  ordtconnlem1  34354  xrge0iifcnv  34363  fsum2dsub  35035  regsfromregtco  37082  fvineqsneu  38090  pibt2  38096  incsequz  38432  equivtotbnd  38462  intidl  38713  keridl  38716  prnc  38751  cdleme50trn123  41361  dva1dim  41792  dia1dim2  41869  3factsumint1  42821  modelac8prim  45734