Theorem anass1rs 651

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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  sossfld  6078  1stconst  7911  infunsdom  9901  creui  11898  qreccl  12638  fsumrlim  15451  fsumo1  15452  climfsum  15460  imasvscaf  17167  grppropd  18509  grpinvpropd  18565  cycsubgcl  18740  frgpup1  19296  ringrghm  19759  phlpropd  20772  mamuass  21459  iccpnfcnv  24013  mbfeqalem1  24710  mbfinf  24734  mbflimsup  24735  mbflimlem  24736  itgfsum  24896  plypf1  25278  mtest  25468  rpvmasum2  26565  ifeqeqx  30786  ordtconnlem1  31776  xrge0iifcnv  31785  fsum2dsub  32487  fvineqsneu  35509  pibt2  35515  incsequz  35833  equivtotbnd  35863  intidl  36114  keridl  36117  prnc  36152  cdleme50trn123  38495  dva1dim  38926  dia1dim2  39003  3factsumint1  39957