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  6037  1stconst  7789  infunsdom  9630  creui  11627  qreccl  12362  fsumrlim  15160  fsumo1  15161  climfsum  15169  imasvscaf  16806  grppropd  18112  grpinvpropd  18168  cycsubgcl  18343  frgpup1  18895  ringrghm  19349  phlpropd  20793  mamuass  21005  iccpnfcnv  23542  mbfeqalem1  24236  mbfinf  24260  mbflimsup  24261  mbflimlem  24262  itgfsum  24421  plypf1  24796  mtest  24986  rpvmasum2  26082  ifeqeqx  30291  ordtconnlem1  31162  xrge0iifcnv  31171  fsum2dsub  31873  fvineqsneu  34686  pibt2  34692  incsequz  35017  equivtotbnd  35050  intidl  35301  keridl  35304  prnc  35339  cdleme50trn123  37684  dva1dim  38115  dia1dim2  38192