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  6159  1stconst  8079  infunsdom  10166  creui  12181  qreccl  12928  fsumrlim  15777  fsumo1  15778  climfsum  15786  imasvscaf  17502  grppropd  18883  grpinvpropd  18947  cycsubgcl  19138  frgpup1  19705  ringrghm  20222  phlpropd  21564  mamuass  22289  iccpnfcnv  24842  mbfeqalem1  25542  mbfinf  25566  mbflimsup  25567  mbflimlem  25568  itgfsum  25728  plypf1  26117  mtest  26313  rpvmasum2  27423  ifeqeqx  32471  ordtconnlem1  33914  xrge0iifcnv  33923  fsum2dsub  34598  fvineqsneu  37399  pibt2  37405  incsequz  37742  equivtotbnd  37772  intidl  38023  keridl  38026  prnc  38061  cdleme50trn123  40548  dva1dim  40979  dia1dim2  41056  3factsumint1  42009  modelac8prim  44982