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  5592  somin2  6128  f1elima  7267  f1imaeq  7269  soisoi  7336  isosolem  7355  xpexr2  7931  smoword  8374  unxpdomlem3  9249  fiming  9492  fiinfg  9493  sornom  10355  fin1a2s  10492  mul4r  11479  mulsub  11759  leltadd  11800  ltord1  11842  leord1  11843  eqord1  11844  divmul24  12021  expcan  14312  ltexp2  14313  bhmafibid2  15636  fsum  15886  fprod  16108  isprm5  16883  ramub  17191  setcinv  18265  grpidpropd  18842  gsumpropd2lem  18868  cmnpropd  20005  gsumcom3  20192  unitpropd  20647  isdrng3lem2  21006  lidl1el  21505  1marepvmarrepid  22890  1marepvsma1  22898  ordtrest2  23522  filuni  24204  haustsms2  24456  blcomps  24712  blcom  24713  metnrmlem3  25181  cnmpopc  25249  icoopnst  25260  icccvx  25271  equivcfil  25620  volcn  25927  dvmptfsum  26295  cxple  27023  cxple3  27029  om2noseqlt2  28686  om2noseqf1o  28687  uhgr2edg  29789  lnosub  31361  chirredlem2  32993  metider  34568  ordtrest2NEW  34597  fsum2dsub  35278  soinfdom  35759  finxpreclem2  38356  fin2so  38573  cover2  38692  filbcmb  38717  isdrngo2  38935  crngohomfo  38983  unichnidl  39008  cdleme50eq  41641  dvhvaddcomN  42196  ismrc  43755  prproropf1olem4  48631  pgnbgreunbgrlem4  49260