Theorem ancom2s 651

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 594	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  662  sotr2  5567  somin2  6093  f1elima  7212  f1imaeq  7214  soisoi  7277  isosolem  7296  xpexr2  7864  smoword  8301  unxpdomlem3  9163  fiming  9408  fiinfg  9409  sornom  10192  fin1a2s  10329  mul4r  11307  mulsub  11585  leltadd  11626  ltord1  11668  leord1  11669  eqord1  11670  divmul24  11850  expcan  14097  ltexp2  14098  bhmafibid2  15397  fsum  15648  fprod  15869  isprm5  16639  ramub  16946  setcinv  18019  grpidpropd  18592  gsumpropd2lem  18609  cmnpropd  19725  gsumcom3  19912  unitpropd  20358  lidl1el  21186  1marepvmarrepid  22524  1marepvsma1  22532  ordtrest2  23153  filuni  23834  haustsms2  24086  blcomps  24342  blcom  24343  metnrmlem3  24811  cnmpopc  24883  icoopnst  24897  icccvx  24909  equivcfil  25260  volcn  25568  dvmptfsum  25940  cxple  26665  cxple3  26671  om2noseqlt2  28301  om2noseqf1o  28302  uhgr2edg  29286  lnosub  30839  chirredlem2  32471  metider  34064  ordtrest2NEW  34093  fsum2dsub  34777  finxpreclem2  37608  fin2so  37821  cover2  37929  filbcmb  37954  isdrngo2  38172  crngohomfo  38220  unichnidl  38245  cdleme50eq  40880  dvhvaddcomN  41435  ismrc  43021  prproropf1olem4  47829  pgnbgreunbgrlem4  48442