Theorem ancom2s 651

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 594	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  662  sotr2  5573  somin2  6099  f1elima  7218  f1imaeq  7220  soisoi  7283  isosolem  7302  xpexr2  7870  smoword  8306  unxpdomlem3  9168  fiming  9413  fiinfg  9414  sornom  10199  fin1a2s  10336  mul4r  11315  mulsub  11593  leltadd  11634  ltord1  11676  leord1  11677  eqord1  11678  divmul24  11859  expcan  14131  ltexp2  14132  bhmafibid2  15431  fsum  15682  fprod  15906  isprm5  16677  ramub  16984  setcinv  18057  grpidpropd  18630  gsumpropd2lem  18647  cmnpropd  19766  gsumcom3  19953  unitpropd  20397  lidl1el  21224  1marepvmarrepid  22540  1marepvsma1  22548  ordtrest2  23169  filuni  23850  haustsms2  24102  blcomps  24358  blcom  24359  metnrmlem3  24827  cnmpopc  24895  icoopnst  24906  icccvx  24917  equivcfil  25266  volcn  25573  dvmptfsum  25942  cxple  26659  cxple3  26665  om2noseqlt2  28292  om2noseqf1o  28293  uhgr2edg  29277  lnosub  30830  chirredlem2  32462  metider  34038  ordtrest2NEW  34067  fsum2dsub  34751  mh-inf3f1  36723  finxpreclem2  37706  fin2so  37928  cover2  38036  filbcmb  38061  isdrngo2  38279  crngohomfo  38327  unichnidl  38352  cdleme50eq  40987  dvhvaddcomN  41542  ismrc  43133  prproropf1olem4  47960  pgnbgreunbgrlem4  48589