Theorem ancom2s 648

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  an42s  659  sotr2  5621  somin2  6141  f1elima  7271  f1imaeq  7273  soisoi  7333  isosolem  7352  xpexr2  7925  smoword  8385  unxpdomlem3  9275  fiming  9521  fiinfg  9522  sornom  10300  fin1a2s  10437  mul4r  11413  mulsub  11687  leltadd  11728  ltord1  11770  leord1  11771  eqord1  11772  divmul24  11948  expcan  14165  ltexp2  14166  bhmafibid2  15445  fsum  15698  fprod  15917  isprm5  16677  ramub  16981  setcinv  18078  grpidpropd  18621  gsumpropd2lem  18638  cmnpropd  19750  gsumcom3  19937  unitpropd  20360  lidl1el  21126  1marepvmarrepid  22507  1marepvsma1  22515  ordtrest2  23138  filuni  23819  haustsms2  24071  blcomps  24329  blcom  24330  metnrmlem3  24807  cnmpopc  24879  icoopnst  24893  icccvx  24905  equivcfil  25257  volcn  25565  dvmptfsum  25937  cxple  26659  cxple3  26665  om2noseqlt2  28207  om2noseqf1o  28208  uhgr2edg  29077  lnosub  30625  chirredlem2  32257  metider  33565  ordtrest2NEW  33594  fsum2dsub  34309  finxpreclem2  36939  fin2so  37150  cover2  37258  filbcmb  37283  isdrngo2  37501  crngohomfo  37549  unichnidl  37574  cdleme50eq  40083  dvhvaddcomN  40638  ismrc  42186  prproropf1olem4  46909