Theorem anass1rs 653

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sossfld  6045  1stconst  7797  infunsdom  9638  creui  11635  qreccl  12371  fsumrlim  15168  fsumo1  15169  climfsum  15177  imasvscaf  16814  grppropd  18120  grpinvpropd  18176  cycsubgcl  18351  frgpup1  18903  ringrghm  19357  phlpropd  20801  mamuass  21013  iccpnfcnv  23550  mbfeqalem1  24244  mbfinf  24268  mbflimsup  24269  mbflimlem  24270  itgfsum  24429  plypf1  24804  mtest  24994  rpvmasum2  26090  ifeqeqx  30299  ordtconnlem1  31169  xrge0iifcnv  31178  fsum2dsub  31880  fvineqsneu  34694  pibt2  34700  incsequz  35025  equivtotbnd  35058  intidl  35309  keridl  35312  prnc  35347  cdleme50trn123  37692  dva1dim  38123  dia1dim2  38200