Theorem anass1rs 646

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 460	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	an32s 643	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  sossfld  5797  1stconst  7502  infunsdom  9324  creui  11307  qreccl  12053  fsumrlim  14881  fsumo1  14882  climfsum  14890  imasvscaf  16514  grppropd  17753  grpinvpropd  17806  cycsubgcl  17933  frgpup1  18503  ringrghm  18921  phlpropd  20324  mamuass  20533  iccpnfcnv  23071  mbfeqalem1  23749  mbfinf  23773  mbflimsup  23774  mbflimlem  23775  itgfsum  23934  plypf1  24309  mtest  24499  rpvmasum2  25553  ifeqeqx  29879  ordtconnlem1  30486  xrge0iifcnv  30495  fsum2dsub  31205  incsequz  34031  equivtotbnd  34064  intidl  34315  keridl  34318  prnc  34353  cdleme50trn123  36575  dva1dim  37006  dia1dim2  37083