Theorem ancom2s 647

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  658  sotr2  5546  somin2  6055  f1elima  7168  f1imaeq  7170  soisoi  7231  isosolem  7250  xpexr2  7802  smoword  8232  unxpdomlem3  9082  fiming  9315  fiinfg  9316  sornom  10093  fin1a2s  10230  mul4r  11204  mulsub  11478  leltadd  11519  ltord1  11561  leord1  11562  eqord1  11563  divmul24  11739  expcan  13947  ltexp2  13948  bhmafibid2  15237  fsum  15491  fprod  15710  isprm5  16471  ramub  16773  setcinv  17864  grpidpropd  18405  gsumpropd2lem  18422  cmnpropd  19455  gsumcom3  19638  unitpropd  19998  lidl1el  20552  1marepvmarrepid  21787  1marepvsma1  21795  ordtrest2  22418  filuni  23099  haustsms2  23351  blcomps  23609  blcom  23610  metnrmlem3  24087  cnmpopc  24154  icoopnst  24165  icccvx  24176  equivcfil  24526  volcn  24833  dvmptfsum  25202  cxple  25913  cxple3  25919  uhgr2edg  27673  lnosub  29219  chirredlem2  30851  metider  31940  ordtrest2NEW  31969  fsum2dsub  32683  finxpreclem2  35619  fin2so  35822  cover2  35930  filbcmb  35956  isdrngo2  36174  crngohomfo  36222  unichnidl  36247  cdleme50eq  38765  dvhvaddcomN  39320  ismrc  40731  prproropf1olem4  45215