Theorem ancom2s 660

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  an42s  671  sotr2  5590  somin2  6122  f1elima  7247  f1imaeq  7249  soisoi  7312  isosolem  7331  xpexr2  7900  smoword  8337  unxpdomlem3  9202  fiming  9444  fiinfg  9445  sornom  10245  fin1a2s  10382  mul4r  11363  mulsub  11641  leltadd  11682  ltord1  11724  leord1  11725  eqord1  11726  divmul24  11906  expcan  14192  ltexp2  14193  bhmafibid2  15506  fsum  15757  fprod  15981  isprm5  16752  ramub  17059  setcinv  18133  grpidpropd  18706  gsumpropd2lem  18723  cmnpropd  19841  gsumcom3  20028  unitpropd  20476  lidl1el  21303  1marepvmarrepid  22642  1marepvsma1  22650  ordtrest2  23271  filuni  23952  haustsms2  24204  blcomps  24460  blcom  24461  metnrmlem3  24929  cnmpopc  24997  icoopnst  25008  icccvx  25019  equivcfil  25368  volcn  25675  dvmptfsum  26044  cxple  26767  cxple3  26773  om2noseqlt2  28400  om2noseqf1o  28401  uhgr2edg  29416  lnosub  30969  chirredlem2  32601  metider  34193  ordtrest2NEW  34222  fsum2dsub  34903  mh-inf3f1  36906  finxpreclem2  37889  fin2so  38111  cover2  38219  filbcmb  38244  isdrngo2  38462  crngohomfo  38510  unichnidl  38535  cdleme50eq  41170  dvhvaddcomN  41725  ismrc  43287  prproropf1olem4  48103  pgnbgreunbgrlem4  48732