Theorem anass1rs 667

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sossfld  6182  1stconst  8091  infunsdom  10192  creui  12209  qreccl  12989  fsumrlim  15859  fsumo1  15860  climfsum  15868  imasvscaf  17589  grppropd  19014  grpinvpropd  19077  cycsubgcl  19273  frgpup1  19841  ringrghm  20392  phlpropd  21770  mamuass  22524  iccpnfcnv  25068  mbfeqalem1  25765  mbfinf  25789  mbflimsup  25790  mbflimlem  25791  itgfsum  25951  plypf1  26334  mtest  26529  rpvmasum2  27638  ifeqeqx  32825  ordtconnlem1  34255  xrge0iifcnv  34264  fsum2dsub  34935  regsfromregtco  36934  fvineqsneu  37940  pibt2  37946  incsequz  38282  equivtotbnd  38312  intidl  38563  keridl  38566  prnc  38601  cdleme50trn123  41213  dva1dim  41644  dia1dim2  41721  3factsumint1  42673  modelac8prim  45588