Theorem ancom2s 649

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 592	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 206  df-an 396

This theorem is referenced by:  an42s  660  sotr2  5616  somin2  6135  f1elima  7267  f1imaeq  7269  soisoi  7330  isosolem  7349  xpexr2  7921  smoword  8380  unxpdomlem3  9268  fiming  9513  fiinfg  9514  sornom  10292  fin1a2s  10429  mul4r  11405  mulsub  11679  leltadd  11720  ltord1  11762  leord1  11763  eqord1  11764  divmul24  11940  expcan  14157  ltexp2  14158  bhmafibid2  15437  fsum  15690  fprod  15909  isprm5  16669  ramub  16973  setcinv  18070  grpidpropd  18613  gsumpropd2lem  18630  cmnpropd  19737  gsumcom3  19924  unitpropd  20345  lidl1el  21111  1marepvmarrepid  22464  1marepvsma1  22472  ordtrest2  23095  filuni  23776  haustsms2  24028  blcomps  24286  blcom  24287  metnrmlem3  24764  cnmpopc  24836  icoopnst  24850  icccvx  24862  equivcfil  25214  volcn  25522  dvmptfsum  25894  cxple  26616  cxple3  26622  om2noseqlt2  28160  om2noseqf1o  28161  uhgr2edg  29008  lnosub  30556  chirredlem2  32188  metider  33431  ordtrest2NEW  33460  fsum2dsub  34175  finxpreclem2  36805  fin2so  37015  cover2  37123  filbcmb  37148  isdrngo2  37366  crngohomfo  37414  unichnidl  37439  cdleme50eq  39951  dvhvaddcomN  40506  ismrc  42043  prproropf1olem4  46769