Theorem ancom2s 650

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an42s  661  sotr2  5561  somin2  6084  f1elima  7200  f1imaeq  7202  soisoi  7265  isosolem  7284  xpexr2  7852  smoword  8289  unxpdomlem3  9147  fiming  9390  fiinfg  9391  sornom  10171  fin1a2s  10308  mul4r  11285  mulsub  11563  leltadd  11604  ltord1  11646  leord1  11647  eqord1  11648  divmul24  11828  expcan  14076  ltexp2  14077  bhmafibid2  15376  fsum  15627  fprod  15848  isprm5  16618  ramub  16925  setcinv  17997  grpidpropd  18536  gsumpropd2lem  18553  cmnpropd  19670  gsumcom3  19857  unitpropd  20302  lidl1el  21133  1marepvmarrepid  22460  1marepvsma1  22468  ordtrest2  23089  filuni  23770  haustsms2  24022  blcomps  24279  blcom  24280  metnrmlem3  24748  cnmpopc  24820  icoopnst  24834  icccvx  24846  equivcfil  25197  volcn  25505  dvmptfsum  25877  cxple  26602  cxple3  26608  om2noseqlt2  28199  om2noseqf1o  28200  uhgr2edg  29153  lnosub  30703  chirredlem2  32335  metider  33867  ordtrest2NEW  33896  fsum2dsub  34581  finxpreclem2  37374  fin2so  37597  cover2  37705  filbcmb  37730  isdrngo2  37948  crngohomfo  37996  unichnidl  38021  cdleme50eq  40530  dvhvaddcomN  41085  ismrc  42684  prproropf1olem4  47500  pgnbgreunbgrlem4  48113