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  4710  xpexr2m  5229  f1elima  5979  f1imaeq  5981  isosolem  6030  caovlem2d  6282  2ndconst  6458  isotilem  7346  prarloclem4  7865  mulsub  8728  leltadd  8775  eqord1  8811  divmul24ap  9047  fprodseq  12352  grpidpropdg  13696  cmnpropd  14100  unitpropdg  14457  blcomps  15499  blcom  15500  dvmptfsum  15828  cxple  16025  cxple3  16029  uhgr2edg  16459