Theorem anass1rs 655

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 652	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  6144  1stconst  8042  infunsdom  10123  creui  12140  qreccl  12882  fsumrlim  15734  fsumo1  15735  climfsum  15743  imasvscaf  17460  grppropd  18881  grpinvpropd  18945  cycsubgcl  19135  frgpup1  19704  ringrghm  20248  phlpropd  21610  mamuass  22346  iccpnfcnv  24898  mbfeqalem1  25598  mbfinf  25622  mbflimsup  25623  mbflimlem  25624  itgfsum  25784  plypf1  26173  mtest  26369  rpvmasum2  27479  ifeqeqx  32617  ordtconnlem1  34081  xrge0iifcnv  34090  fsum2dsub  34764  regsfromregtr  36668  fvineqsneu  37616  pibt2  37622  incsequz  37949  equivtotbnd  37979  intidl  38230  keridl  38233  prnc  38268  cdleme50trn123  40814  dva1dim  41245  dia1dim2  41322  3factsumint1  42275  modelac8prim  45233