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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  sossfld  6012  1stconst  7814  infunsdom  9707  creui  11704  qreccl  12444  fsumrlim  15252  fsumo1  15253  climfsum  15261  imasvscaf  16908  grppropd  18229  grpinvpropd  18285  cycsubgcl  18460  frgpup1  19012  ringrghm  19470  phlpropd  20464  mamuass  21146  iccpnfcnv  23689  mbfeqalem1  24386  mbfinf  24410  mbflimsup  24411  mbflimlem  24412  itgfsum  24571  plypf1  24953  mtest  25143  rpvmasum2  26240  ifeqeqx  30451  ordtconnlem1  31438  xrge0iifcnv  31447  fsum2dsub  32149  fvineqsneu  35194  pibt2  35200  incsequz  35518  equivtotbnd  35548  intidl  35799  keridl  35802  prnc  35837  cdleme50trn123  38180  dva1dim  38611  dia1dim2  38688  3factsumint1  39638