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  6152  1stconst  8052  infunsdom  10135  creui  12152  qreccl  12894  fsumrlim  15746  fsumo1  15747  climfsum  15755  imasvscaf  17472  grppropd  18893  grpinvpropd  18957  cycsubgcl  19147  frgpup1  19716  ringrghm  20260  phlpropd  21622  mamuass  22358  iccpnfcnv  24910  mbfeqalem1  25610  mbfinf  25634  mbflimsup  25635  mbflimlem  25636  itgfsum  25796  plypf1  26185  mtest  26381  rpvmasum2  27491  ifeqeqx  32628  ordtconnlem1  34101  xrge0iifcnv  34110  fsum2dsub  34784  regsfromregtr  36687  fvineqsneu  37663  pibt2  37669  incsequz  37996  equivtotbnd  38026  intidl  38277  keridl  38280  prnc  38315  cdleme50trn123  40927  dva1dim  41358  dia1dim2  41435  3factsumint1  42388  modelac8prim  45345