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  4661  xpexr2m  5178  f1elima  5914  f1imaeq  5916  isosolem  5965  caovlem2d  6215  2ndconst  6387  isotilem  7205  prarloclem4  7718  mulsub  8580  leltadd  8627  eqord1  8663  divmul24ap  8896  fprodseq  12146  grpidpropdg  13459  cmnpropd  13884  unitpropdg  14165  blcomps  15123  blcom  15124  dvmptfsum  15452  cxple  15644  cxple3  15648  uhgr2edg  16060