Theorem anass1rs 652

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  sossfld  6094  1stconst  7949  infunsdom  9979  creui  11977  qreccl  12718  fsumrlim  15532  fsumo1  15533  climfsum  15541  imasvscaf  17259  grppropd  18603  grpinvpropd  18659  cycsubgcl  18834  frgpup1  19390  ringrghm  19853  phlpropd  20869  mamuass  21558  iccpnfcnv  24116  mbfeqalem1  24814  mbfinf  24838  mbflimsup  24839  mbflimlem  24840  itgfsum  25000  plypf1  25382  mtest  25572  rpvmasum2  26669  ifeqeqx  30894  ordtconnlem1  31883  xrge0iifcnv  31892  fsum2dsub  32596  fvineqsneu  35591  pibt2  35597  incsequz  35915  equivtotbnd  35945  intidl  36196  keridl  36199  prnc  36234  cdleme50trn123  38575  dva1dim  39006  dia1dim2  39083  3factsumint1  40036