Theorem anass1rs 651

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  sossfld  6184  1stconst  8088  infunsdom  10211  creui  12211  qreccl  12957  fsumrlim  15761  fsumo1  15762  climfsum  15770  imasvscaf  17489  grppropd  18873  grpinvpropd  18934  cycsubgcl  19121  frgpup1  19684  ringrghm  20201  phlpropd  21427  mamuass  22122  iccpnfcnv  24689  mbfeqalem1  25390  mbfinf  25414  mbflimsup  25415  mbflimlem  25416  itgfsum  25576  plypf1  25961  mtest  26152  rpvmasum2  27251  ifeqeqx  32041  ordtconnlem1  33202  xrge0iifcnv  33211  fsum2dsub  33917  fvineqsneu  36595  pibt2  36601  incsequz  36919  equivtotbnd  36949  intidl  37200  keridl  37203  prnc  37238  cdleme50trn123  39728  dva1dim  40159  dia1dim2  40236  3factsumint1  41192