Theorem anass1rs 634

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

Syntax hints:   → wi 4   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  sossfld  5720  infunsdom  9242  creui  11221  qreccl  12016  fsumrlim  14750  fsumo1  14751  climfsum  14759  imasvscaf  16407  grppropd  17645  grpinvpropd  17698  cycsubgcl  17828  frgpup1  18395  ringrghm  18813  phlpropd  20217  mamuass  20425  iccpnfcnv  22963  mbfeqalem  23629  mbfinf  23652  mbflimsup  23653  mbflimlem  23654  itgfsum  23813  plypf1  24188  mtest  24378  rpvmasum2  25422  ifeqeqx  29699  ordtconnlem1  30310  xrge0iifcnv  30319  fsum2dsub  31025  incsequz  33874  equivtotbnd  33907  intidl  34158  keridl  34161  prnc  34196  cdleme50trn123  36362  dva1dim  36793  dia1dim2  36870