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  7211  f1imaeq  7213  soisoi  7276  isosolem  7295  xpexr2  7863  smoword  8300  unxpdomlem3  9162  fiming  9407  fiinfg  9408  sornom  10191  fin1a2s  10328  mul4r  11306  mulsub  11584  leltadd  11625  ltord1  11667  leord1  11668  eqord1  11669  divmul24  11849  expcan  14096  ltexp2  14097  bhmafibid2  15396  fsum  15647  fprod  15868  isprm5  16638  ramub  16945  setcinv  18018  grpidpropd  18591  gsumpropd2lem  18608  cmnpropd  19724  gsumcom3  19911  unitpropd  20357  lidl1el  21185  1marepvmarrepid  22523  1marepvsma1  22531  ordtrest2  23152  filuni  23833  haustsms2  24085  blcomps  24341  blcom  24342  metnrmlem3  24810  cnmpopc  24882  icoopnst  24896  icccvx  24908  equivcfil  25259  volcn  25567  dvmptfsum  25939  cxple  26664  cxple3  26670  om2noseqlt2  28281  om2noseqf1o  28282  uhgr2edg  29264  lnosub  30817  chirredlem2  32449  metider  34032  ordtrest2NEW  34061  fsum2dsub  34745  finxpreclem2  37566  fin2so  37779  cover2  37887  filbcmb  37912  isdrngo2  38130  crngohomfo  38178  unichnidl  38203  cdleme50eq  40838  dvhvaddcomN  41393  ismrc  42979  prproropf1olem4  47788  pgnbgreunbgrlem4  48401