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  5601  somin2  6133  f1elima  7263  f1imaeq  7265  soisoi  7332  isosolem  7351  xpexr2  7919  smoword  8358  unxpdomlem3  9231  fiming  9473  fiinfg  9474  sornom  10282  fin1a2s  10419  mul4r  11406  mulsub  11684  leltadd  11725  ltord1  11767  leord1  11768  eqord1  11769  divmul24  11946  expcan  14235  ltexp2  14236  bhmafibid2  15558  fsum  15808  fprod  16032  isprm5  16802  ramub  17109  setcinv  18183  grpidpropd  18759  gsumpropd2lem  18783  cmnpropd  19919  gsumcom3  20106  unitpropd  20559  isdrng3lem2  20916  lidl1el  21415  1marepvmarrepid  22798  1marepvsma1  22806  ordtrest2  23430  filuni  24112  haustsms2  24364  blcomps  24620  blcom  24621  metnrmlem3  25089  cnmpopc  25157  icoopnst  25168  icccvx  25179  equivcfil  25528  volcn  25835  dvmptfsum  26204  cxple  26930  cxple3  26936  om2noseqlt2  28563  om2noseqf1o  28564  uhgr2edg  29654  lnosub  31226  chirredlem2  32858  metider  34391  ordtrest2NEW  34420  fsum2dsub  35102  mh-inf3f1  37147  finxpreclem2  38131  fin2so  38348  cover2  38452  filbcmb  38477  isdrngo2  38695  crngohomfo  38743  unichnidl  38768  cdleme50eq  41401  dvhvaddcomN  41956  ismrc  43533  prproropf1olem4  48393  pgnbgreunbgrlem4  49022