Theorem anass1rs 656

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 653	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 207  df-an 396

This theorem is referenced by:  sossfld  6150  1stconst  8050  infunsdom  10135  creui  12154  qreccl  12919  fsumrlim  15774  fsumo1  15775  climfsum  15783  imasvscaf  17503  grppropd  18927  grpinvpropd  18991  cycsubgcl  19181  frgpup1  19750  ringrghm  20294  phlpropd  21635  mamuass  22367  iccpnfcnv  24911  mbfeqalem1  25608  mbfinf  25632  mbflimsup  25633  mbflimlem  25634  itgfsum  25794  plypf1  26177  mtest  26369  rpvmasum2  27475  ifeqeqx  32612  ordtconnlem1  34068  xrge0iifcnv  34077  fsum2dsub  34751  regsfromregtco  36720  fvineqsneu  37727  pibt2  37733  incsequz  38069  equivtotbnd  38099  intidl  38350  keridl  38353  prnc  38388  cdleme50trn123  41000  dva1dim  41431  dia1dim2  41508  3factsumint1  42460  modelac8prim  45419