Theorem anass1rs 654

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 651	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  6010  1stconst  7778  infunsdom  9625  creui  11620  qreccl  12356  fsumrlim  15158  fsumo1  15159  climfsum  15167  imasvscaf  16804  grppropd  18110  grpinvpropd  18166  cycsubgcl  18341  frgpup1  18893  ringrghm  19351  phlpropd  20344  mamuass  21007  iccpnfcnv  23549  mbfeqalem1  24245  mbfinf  24269  mbflimsup  24270  mbflimlem  24271  itgfsum  24430  plypf1  24809  mtest  24999  rpvmasum2  26096  ifeqeqx  30309  ordtconnlem1  31277  xrge0iifcnv  31286  fsum2dsub  31988  fvineqsneu  34828  pibt2  34834  incsequz  35186  equivtotbnd  35216  intidl  35467  keridl  35470  prnc  35505  cdleme50trn123  37850  dva1dim  38281  dia1dim2  38358  3factsumint1  39309