Theorem ancom2s 662

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  an42s  673  sotr2  5603  somin2  6135  f1elima  7261  f1imaeq  7263  soisoi  7326  isosolem  7345  xpexr2  7915  smoword  8352  unxpdomlem3  9217  fiming  9459  fiinfg  9460  sornom  10260  fin1a2s  10397  mul4r  11378  mulsub  11656  leltadd  11697  ltord1  11739  leord1  11740  eqord1  11741  divmul24  11918  expcan  14204  ltexp2  14205  bhmafibid2  15519  fsum  15770  fprod  15994  isprm5  16765  ramub  17072  setcinv  18146  grpidpropd  18719  gsumpropd2lem  18736  cmnpropd  19860  gsumcom3  20047  unitpropd  20498  lidl1el  21330  1marepvmarrepid  22711  1marepvsma1  22719  ordtrest2  23340  filuni  24021  haustsms2  24273  blcomps  24529  blcom  24530  metnrmlem3  24998  cnmpopc  25066  icoopnst  25077  icccvx  25088  equivcfil  25437  volcn  25744  dvmptfsum  26113  cxple  26836  cxple3  26842  om2noseqlt2  28469  om2noseqf1o  28470  uhgr2edg  29524  lnosub  31077  chirredlem2  32709  metider  34250  ordtrest2NEW  34279  fsum2dsub  34960  mh-inf3f1  36996  finxpreclem2  37980  fin2so  38202  cover2  38310  filbcmb  38335  isdrngo2  38553  crngohomfo  38601  unichnidl  38626  cdleme50eq  41261  dvhvaddcomN  41816  ismrc  43380  prproropf1olem4  48200  pgnbgreunbgrlem4  48829