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  4663  xpexr2m  5180  f1elima  5919  f1imaeq  5921  isosolem  5970  caovlem2d  6220  2ndconst  6392  isotilem  7210  prarloclem4  7723  mulsub  8585  leltadd  8632  eqord1  8668  divmul24ap  8901  fprodseq  12167  grpidpropdg  13480  cmnpropd  13905  unitpropdg  14186  blcomps  15149  blcom  15150  dvmptfsum  15478  cxple  15670  cxple3  15674  uhgr2edg  16086