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  5629  somin2  6157  f1elima  7282  f1imaeq  7284  soisoi  7347  isosolem  7366  xpexr2  7941  smoword  8404  unxpdomlem3  9285  fiming  9535  fiinfg  9536  sornom  10314  fin1a2s  10451  mul4r  11427  mulsub  11703  leltadd  11744  ltord1  11786  leord1  11787  eqord1  11788  divmul24  11968  expcan  14205  ltexp2  14206  bhmafibid2  15501  fsum  15752  fprod  15973  isprm5  16740  ramub  17046  setcinv  18143  grpidpropd  18687  gsumpropd2lem  18704  cmnpropd  19823  gsumcom3  20010  unitpropd  20433  lidl1el  21253  1marepvmarrepid  22596  1marepvsma1  22604  ordtrest2  23227  filuni  23908  haustsms2  24160  blcomps  24418  blcom  24419  metnrmlem3  24896  cnmpopc  24968  icoopnst  24982  icccvx  24994  equivcfil  25346  volcn  25654  dvmptfsum  26027  cxple  26751  cxple3  26757  om2noseqlt2  28320  om2noseqf1o  28321  uhgr2edg  29239  lnosub  30787  chirredlem2  32419  metider  33854  ordtrest2NEW  33883  fsum2dsub  34600  finxpreclem2  37372  fin2so  37593  cover2  37701  filbcmb  37726  isdrngo2  37944  crngohomfo  37992  unichnidl  38017  cdleme50eq  40523  dvhvaddcomN  41078  ismrc  42688  prproropf1olem4  47430