Theorem anass1rs 656

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sossfld  6144  1stconst  8043  infunsdom  10126  creui  12145  qreccl  12910  fsumrlim  15765  fsumo1  15766  climfsum  15774  imasvscaf  17494  grppropd  18918  grpinvpropd  18982  cycsubgcl  19172  frgpup1  19741  ringrghm  20285  phlpropd  21645  mamuass  22377  iccpnfcnv  24921  mbfeqalem1  25618  mbfinf  25642  mbflimsup  25643  mbflimlem  25644  itgfsum  25804  plypf1  26187  mtest  26382  rpvmasum2  27489  ifeqeqx  32627  ordtconnlem1  34084  xrge0iifcnv  34093  fsum2dsub  34767  regsfromregtco  36736  fvineqsneu  37741  pibt2  37747  incsequz  38083  equivtotbnd  38113  intidl  38364  keridl  38367  prnc  38402  cdleme50trn123  41014  dva1dim  41445  dia1dim2  41522  3factsumint1  42474  modelac8prim  45437