Theorem ancom2s 663

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an42s  674  sotr2  5597  somin2  6141  f1elima  7290  f1imaeq  7292  soisoi  7359  isosolem  7378  xpexr2  7955  smoword  8402  unxpdomlem3  9277  fiming  9519  fiinfg  9520  sornom  10382  fin1a2s  10519  mul4r  11506  mulsub  11786  leltadd  11827  ltord1  11869  leord1  11870  eqord1  11871  divmul24  12048  expcan  14339  ltexp2  14340  bhmafibid2  15665  fsum  15915  fprod  16137  isprm5  16912  ramub  17220  setcinv  18294  grpidpropd  18871  gsumpropd2lem  18897  cmnpropd  20035  gsumcom3  20222  unitpropd  20677  isdrng3lem2  21036  lidl1el  21535  1marepvmarrepid  22920  1marepvsma1  22928  ordtrest2  23552  filuni  24234  haustsms2  24486  blcomps  24742  blcom  24743  metnrmlem3  25211  cnmpopc  25279  icoopnst  25290  icccvx  25301  equivcfil  25650  volcn  25957  dvmptfsum  26325  cxple  27053  cxple3  27059  om2noseqlt2  28716  om2noseqf1o  28717  uhgr2edg  29819  lnosub  31391  chirredlem2  33023  metider  34596  ordtrest2NEW  34625  fsum2dsub  35306  soinfdom  35800  finxpreclem2  38505  fin2so  38722  cover2  38841  filbcmb  38866  isdrngo2  39084  crngohomfo  39132  unichnidl  39157  cdleme50eq  41790  dvhvaddcomN  42345  ismrc  43905  prproropf1olem4  48793  pgnbgreunbgrlem4  49422