Theorem ancom2s 572

Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
an12s.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
ancom2s	⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)

Proof of Theorem ancom2s

Step	Hyp	Ref	Expression
1		pm3.22 265	. 2 ⊢ ((𝜒 ∧ 𝜓) → (𝜓 ∧ 𝜒))
2		an12s.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 286	1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  an42s  597  ordsuc  4708  xpexr2m  5227  f1elima  5973  f1imaeq  5975  isosolem  6024  caovlem2d  6276  2ndconst  6452  isotilem  7340  prarloclem4  7859  mulsub  8722  leltadd  8769  eqord1  8805  divmul24ap  9040  fprodseq  12333  grpidpropdg  13677  cmnpropd  14081  unitpropdg  14438  blcomps  15480  blcom  15481  dvmptfsum  15809  cxple  16002  cxple3  16006  uhgr2edg  16430