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 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  an42s  597  ordsuc  4712  xpexr2m  5232  f1elima  5982  f1imaeq  5984  isosolem  6033  caovlem2d  6285  2ndconst  6462  isotilem  7353  prarloclem4  7872  mulsub  8736  leltadd  8783  eqord1  8819  divmul24ap  9055  fprodseq  12376  grpidpropdg  13754  cmnpropd  14189  unitpropdg  14565  blcomps  15634  blcom  15635  dvmptfsum  15963  cxple  16164  cxple3  16168  uhgr2edg  16664