Theorem anass1rs 654

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 651	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  6217  1stconst  8141  infunsdom  10282  creui  12288  qreccl  13034  fsumrlim  15859  fsumo1  15860  climfsum  15868  imasvscaf  17599  grppropd  18991  grpinvpropd  19055  cycsubgcl  19246  frgpup1  19817  ringrghm  20336  phlpropd  21696  mamuass  22427  iccpnfcnv  24994  mbfeqalem1  25695  mbfinf  25719  mbflimsup  25720  mbflimlem  25721  itgfsum  25882  plypf1  26271  mtest  26465  rpvmasum2  27574  ifeqeqx  32565  ordtconnlem1  33870  xrge0iifcnv  33879  fsum2dsub  34584  fvineqsneu  37377  pibt2  37383  incsequz  37708  equivtotbnd  37738  intidl  37989  keridl  37992  prnc  38027  cdleme50trn123  40511  dva1dim  40942  dia1dim2  41019  3factsumint1  41978