Theorem anass1rs 667

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  sossfld  6184  1stconst  8091  infunsdom  10192  creui  12208  qreccl  12988  fsumrlim  15859  fsumo1  15860  climfsum  15868  imasvscaf  17588  grppropd  19013  grpinvpropd  19076  cycsubgcl  19272  frgpup1  19840  ringrghm  20392  phlpropd  21805  mamuass  22559  iccpnfcnv  25103  mbfeqalem1  25800  mbfinf  25824  mbflimsup  25825  mbflimlem  25826  itgfsum  25986  plypf1  26369  mtest  26567  rpvmasum2  27676  ifeqeqx  32888  ordtconnlem1  34314  xrge0iifcnv  34323  fsum2dsub  34994  regsfromregtco  37049  fvineqsneu  38057  pibt2  38063  incsequz  38399  equivtotbnd  38429  intidl  38680  keridl  38683  prnc  38718  cdleme50trn123  41328  dva1dim  41759  dia1dim2  41836  3factsumint1  42788  modelac8prim  45701