Theorem ancom2s 648

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  an42s  659  sotr2  5582  somin2  6094  f1elima  7215  f1imaeq  7217  soisoi  7278  isosolem  7297  xpexr2  7861  smoword  8317  unxpdomlem3  9203  fiming  9443  fiinfg  9444  sornom  10222  fin1a2s  10359  mul4r  11333  mulsub  11607  leltadd  11648  ltord1  11690  leord1  11691  eqord1  11692  divmul24  11868  expcan  14084  ltexp2  14085  bhmafibid2  15363  fsum  15616  fprod  15835  isprm5  16594  ramub  16896  setcinv  17990  grpidpropd  18531  gsumpropd2lem  18548  cmnpropd  19587  gsumcom3  19769  unitpropd  20142  lidl1el  20747  1marepvmarrepid  21961  1marepvsma1  21969  ordtrest2  22592  filuni  23273  haustsms2  23525  blcomps  23783  blcom  23784  metnrmlem3  24261  cnmpopc  24328  icoopnst  24339  icccvx  24350  equivcfil  24700  volcn  25007  dvmptfsum  25376  cxple  26087  cxple3  26093  uhgr2edg  28219  lnosub  29764  chirredlem2  31396  metider  32564  ordtrest2NEW  32593  fsum2dsub  33309  finxpreclem2  35934  fin2so  36138  cover2  36246  filbcmb  36272  isdrngo2  36490  crngohomfo  36538  unichnidl  36563  cdleme50eq  39077  dvhvaddcomN  39632  ismrc  41082  prproropf1olem4  45818