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  6139  1stconst  8040  infunsdom  10126  creui  12141  qreccl  12888  fsumrlim  15736  fsumo1  15737  climfsum  15745  imasvscaf  17461  grppropd  18848  grpinvpropd  18912  cycsubgcl  19103  frgpup1  19672  ringrghm  20216  phlpropd  21580  mamuass  22305  iccpnfcnv  24858  mbfeqalem1  25558  mbfinf  25582  mbflimsup  25583  mbflimlem  25584  itgfsum  25744  plypf1  26133  mtest  26329  rpvmasum2  27439  ifeqeqx  32504  ordtconnlem1  33893  xrge0iifcnv  33902  fsum2dsub  34577  fvineqsneu  37387  pibt2  37393  incsequz  37730  equivtotbnd  37760  intidl  38011  keridl  38014  prnc  38049  cdleme50trn123  40536  dva1dim  40967  dia1dim2  41044  3factsumint1  41997  modelac8prim  44969