Theorem ancom2s 566

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  591  ordsuc  4659  xpexr2m  5176  f1elima  5909  f1imaeq  5911  isosolem  5960  caovlem2d  6210  2ndconst  6382  isotilem  7199  prarloclem4  7711  mulsub  8573  leltadd  8620  eqord1  8656  divmul24ap  8889  fprodseq  12137  grpidpropdg  13450  cmnpropd  13875  unitpropdg  14155  blcomps  15113  blcom  15114  dvmptfsum  15442  cxple  15634  cxple3  15638  uhgr2edg  16050