Theorem ancom2s 568

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  593  ordsuc  4687  xpexr2m  5206  f1elima  5948  f1imaeq  5950  isosolem  5999  caovlem2d  6249  2ndconst  6420  isotilem  7299  prarloclem4  7818  mulsub  8679  leltadd  8726  eqord1  8762  divmul24ap  8995  fprodseq  12277  grpidpropdg  13608  cmnpropd  14033  unitpropdg  14315  blcomps  15310  blcom  15311  dvmptfsum  15639  cxple  15831  cxple3  15835  uhgr2edg  16250