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  6133  1stconst  8030  infunsdom  10104  creui  12120  qreccl  12867  fsumrlim  15718  fsumo1  15719  climfsum  15727  imasvscaf  17443  grppropd  18864  grpinvpropd  18928  cycsubgcl  19119  frgpup1  19688  ringrghm  20232  phlpropd  21593  mamuass  22318  iccpnfcnv  24870  mbfeqalem1  25570  mbfinf  25594  mbflimsup  25595  mbflimlem  25596  itgfsum  25756  plypf1  26145  mtest  26341  rpvmasum2  27451  ifeqeqx  32520  ordtconnlem1  33935  xrge0iifcnv  33944  fsum2dsub  34618  fvineqsneu  37451  pibt2  37457  incsequz  37794  equivtotbnd  37824  intidl  38075  keridl  38078  prnc  38113  cdleme50trn123  40599  dva1dim  41030  dia1dim2  41107  3factsumint1  42060  modelac8prim  45031