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  19118  frgpup1  19687  ringrghm  20231  phlpropd  21592  mamuass  22317  iccpnfcnv  24869  mbfeqalem1  25569  mbfinf  25593  mbflimsup  25594  mbflimlem  25595  itgfsum  25755  plypf1  26144  mtest  26340  rpvmasum2  27450  ifeqeqx  32522  ordtconnlem1  33937  xrge0iifcnv  33946  fsum2dsub  34620  fvineqsneu  37455  pibt2  37461  incsequz  37787  equivtotbnd  37817  intidl  38068  keridl  38071  prnc  38106  cdleme50trn123  40652  dva1dim  41083  dia1dim2  41160  3factsumint1  42113  modelac8prim  45084