Theorem anass1rs 665

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  sossfld  6167  1stconst  8073  infunsdom  10163  creui  12184  qreccl  12964  fsumrlim  15830  fsumo1  15831  climfsum  15839  imasvscaf  17560  grppropd  18984  grpinvpropd  19048  cycsubgcl  19238  frgpup1  19806  ringrghm  20350  phlpropd  21695  mamuass  22450  iccpnfcnv  24994  mbfeqalem1  25691  mbfinf  25715  mbflimsup  25716  mbflimlem  25717  itgfsum  25877  plypf1  26260  mtest  26455  rpvmasum2  27564  ifeqeqx  32701  ordtconnlem1  34182  xrge0iifcnv  34191  fsum2dsub  34862  regsfromregtco  36859  fvineqsneu  37866  pibt2  37872  incsequz  38208  equivtotbnd  38238  intidl  38489  keridl  38492  prnc  38527  cdleme50trn123  41139  dva1dim  41570  dia1dim2  41647  3factsumint1  42599  modelac8prim  45529