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 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  657  sotr2  5619  somin2  6135  f1elima  7264  f1imaeq  7266  soisoi  7327  isosolem  7346  xpexr2  7912  smoword  8368  unxpdomlem3  9254  fiming  9495  fiinfg  9496  sornom  10274  fin1a2s  10411  mul4r  11387  mulsub  11661  leltadd  11702  ltord1  11744  leord1  11745  eqord1  11746  divmul24  11922  expcan  14138  ltexp2  14139  bhmafibid2  15417  fsum  15670  fprod  15889  isprm5  16648  ramub  16950  setcinv  18044  grpidpropd  18587  gsumpropd2lem  18604  cmnpropd  19700  gsumcom3  19887  unitpropd  20308  lidl1el  20990  1marepvmarrepid  22297  1marepvsma1  22305  ordtrest2  22928  filuni  23609  haustsms2  23861  blcomps  24119  blcom  24120  metnrmlem3  24597  cnmpopc  24669  icoopnst  24683  icccvx  24695  equivcfil  25047  volcn  25355  dvmptfsum  25727  cxple  26439  cxple3  26445  uhgr2edg  28732  lnosub  30279  chirredlem2  31911  metider  33172  ordtrest2NEW  33201  fsum2dsub  33917  finxpreclem2  36574  fin2so  36778  cover2  36886  filbcmb  36911  isdrngo2  37129  crngohomfo  37177  unichnidl  37202  cdleme50eq  39715  dvhvaddcomN  40270  ismrc  41741  prproropf1olem4  46472