Theorem ancom2s 646

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  657  sotr2  5526  somin2  6029  f1elima  7117  f1imaeq  7119  soisoi  7179  isosolem  7198  xpexr2  7740  smoword  8168  unxpdomlem3  8958  fiming  9187  fiinfg  9188  sornom  9964  fin1a2s  10101  mul4r  11074  mulsub  11348  leltadd  11389  ltord1  11431  leord1  11432  eqord1  11433  divmul24  11609  expcan  13815  ltexp2  13816  bhmafibid2  15106  fsum  15360  fprod  15579  isprm5  16340  ramub  16642  setcinv  17721  grpidpropd  18261  gsumpropd2lem  18278  cmnpropd  19311  gsumcom3  19494  unitpropd  19854  lidl1el  20402  1marepvmarrepid  21632  1marepvsma1  21640  ordtrest2  22263  filuni  22944  haustsms2  23196  blcomps  23454  blcom  23455  metnrmlem3  23930  cnmpopc  23997  icoopnst  24008  icccvx  24019  equivcfil  24368  volcn  24675  dvmptfsum  25044  cxple  25755  cxple3  25761  uhgr2edg  27478  lnosub  29022  chirredlem2  30654  metider  31746  ordtrest2NEW  31775  fsum2dsub  32487  finxpreclem2  35488  fin2so  35691  cover2  35799  filbcmb  35825  isdrngo2  36043  crngohomfo  36091  unichnidl  36116  cdleme50eq  38482  dvhvaddcomN  39037  ismrc  40439  prproropf1olem4  44846