Theorem anass1rs 655

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 652	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  6141  1stconst  8039  infunsdom  10115  creui  12131  qreccl  12873  fsumrlim  15725  fsumo1  15726  climfsum  15734  imasvscaf  17451  grppropd  18872  grpinvpropd  18936  cycsubgcl  19126  frgpup1  19695  ringrghm  20239  phlpropd  21601  mamuass  22337  iccpnfcnv  24889  mbfeqalem1  25589  mbfinf  25613  mbflimsup  25614  mbflimlem  25615  itgfsum  25775  plypf1  26164  mtest  26360  rpvmasum2  27470  ifeqeqx  32543  ordtconnlem1  34009  xrge0iifcnv  34018  fsum2dsub  34692  fvineqsneu  37528  pibt2  37534  incsequz  37861  equivtotbnd  37891  intidl  38142  keridl  38145  prnc  38180  cdleme50trn123  40726  dva1dim  41157  dia1dim2  41234  3factsumint1  42187  modelac8prim  45149