Theorem anass1rs 845

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  sossfld  5499  infunsdom  8919  creui  10892  qreccl  11684  fsumrlim  14384  fsumo1  14385  climfsum  14393  imasvscaf  16022  grppropd  17260  grpinvpropd  17313  cycsubgcl  17443  frgpup1  18011  ringrghm  18428  phlpropd  19819  mamuass  20027  iccpnfcnv  22551  mbfeqalem  23215  mbfinf  23238  mbflimsup  23239  mbflimlem  23240  itgfsum  23399  plypf1  23772  mtest  23962  rpvmasum2  25001  ifeqeqx  28745  ordtconlem1  29298  xrge0iifcnv  29307  incsequz  32714  equivtotbnd  32747  intidl  32998  keridl  33001  prnc  33036  cdleme50trn123  34860  dva1dim  35291  dia1dim2  35369