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  6180  1stconst  8104  infunsdom  10232  creui  12240  qreccl  12990  fsumrlim  15832  fsumo1  15833  climfsum  15841  imasvscaf  17558  grppropd  18939  grpinvpropd  19003  cycsubgcl  19194  frgpup1  19761  ringrghm  20278  phlpropd  21620  mamuass  22345  iccpnfcnv  24898  mbfeqalem1  25599  mbfinf  25623  mbflimsup  25624  mbflimlem  25625  itgfsum  25785  plypf1  26174  mtest  26370  rpvmasum2  27480  ifeqeqx  32528  ordtconnlem1  33960  xrge0iifcnv  33969  fsum2dsub  34644  fvineqsneu  37434  pibt2  37440  incsequz  37777  equivtotbnd  37807  intidl  38058  keridl  38061  prnc  38096  cdleme50trn123  40578  dva1dim  41009  dia1dim2  41086  3factsumint1  42039  modelac8prim  44984