Theorem ancom2s 650

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

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  an42s  661  sotr2  5580  somin2  6108  f1elima  7238  f1imaeq  7240  soisoi  7303  isosolem  7322  xpexr2  7895  smoword  8335  unxpdomlem3  9199  fiming  9451  fiinfg  9452  sornom  10230  fin1a2s  10367  mul4r  11343  mulsub  11621  leltadd  11662  ltord1  11704  leord1  11705  eqord1  11706  divmul24  11886  expcan  14134  ltexp2  14135  bhmafibid2  15435  fsum  15686  fprod  15907  isprm5  16677  ramub  16984  setcinv  18052  grpidpropd  18589  gsumpropd2lem  18606  cmnpropd  19721  gsumcom3  19908  unitpropd  20326  lidl1el  21136  1marepvmarrepid  22462  1marepvsma1  22470  ordtrest2  23091  filuni  23772  haustsms2  24024  blcomps  24281  blcom  24282  metnrmlem3  24750  cnmpopc  24822  icoopnst  24836  icccvx  24848  equivcfil  25199  volcn  25507  dvmptfsum  25879  cxple  26604  cxple3  26610  om2noseqlt2  28194  om2noseqf1o  28195  uhgr2edg  29135  lnosub  30688  chirredlem2  32320  metider  33884  ordtrest2NEW  33913  fsum2dsub  34598  finxpreclem2  37378  fin2so  37601  cover2  37709  filbcmb  37734  isdrngo2  37952  crngohomfo  38000  unichnidl  38025  cdleme50eq  40535  dvhvaddcomN  41090  ismrc  42689  prproropf1olem4  47507  pgnbgreunbgrlem4  48109