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  6196  1stconst  8148  infunsdom  10330  creui  12355  qreccl  13137  fsumrlim  16022  fsumo1  16023  climfsum  16031  imasvscaf  17761  grppropd  19212  grpinvpropd  19275  cycsubgcl  19471  frgpup1  20040  ringrghm  20595  phlpropd  22016  mamuass  22772  iccpnfcnv  25320  mbfeqalem1  26017  mbfinf  26041  mbflimsup  26042  mbflimlem  26043  itgfsum  26202  plypf1  26586  mtest  26788  rpvmasum2  27896  ifeqeqx  33236  ordtconnlem1  34667  xrge0iifcnv  34676  fsum2dsub  35347  regsfromregtco  37541  fvineqsneu  38602  pibt2  38608  incsequz  38948  equivtotbnd  38978  intidl  39229  keridl  39232  prnc  39267  cdleme50trn123  41877  dva1dim  42308  dia1dim2  42385  3factsumint1  43337  modelac8prim  46246