Theorem ancom2s 662

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 464	. 2 ⊢ ((𝜒 ∧ 𝜓) → (𝜓 ∧ 𝜒))
2		an12s.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 604	1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  an42s  673  sotr2  5602  somin2  6134  f1elima  7261  f1imaeq  7263  soisoi  7326  isosolem  7345  xpexr2  7914  smoword  8351  unxpdomlem3  9216  fiming  9458  fiinfg  9459  sornom  10267  fin1a2s  10404  mul4r  11385  mulsub  11663  leltadd  11704  ltord1  11746  leord1  11747  eqord1  11748  divmul24  11925  expcan  14212  ltexp2  14213  bhmafibid2  15527  fsum  15778  fprod  16002  isprm5  16772  ramub  17079  setcinv  18153  grpidpropd  18726  gsumpropd2lem  18743  cmnpropd  19867  gsumcom3  20054  unitpropd  20506  isdrng3lem2  20863  lidl1el  21362  1marepvmarrepid  22743  1marepvsma1  22751  ordtrest2  23372  filuni  24053  haustsms2  24305  blcomps  24561  blcom  24562  metnrmlem3  25030  cnmpopc  25098  icoopnst  25109  icccvx  25120  equivcfil  25469  volcn  25776  dvmptfsum  26145  cxple  26871  cxple3  26877  om2noseqlt2  28504  om2noseqf1o  28505  uhgr2edg  29569  lnosub  31122  chirredlem2  32754  metider  34293  ordtrest2NEW  34322  fsum2dsub  35003  mh-inf3f1  37080  finxpreclem2  38064  fin2so  38286  cover2  38394  filbcmb  38419  isdrngo2  38637  crngohomfo  38685  unichnidl  38710  cdleme50eq  41343  dvhvaddcomN  41898  ismrc  43460  prproropf1olem4  48283  pgnbgreunbgrlem4  48912