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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  an42s  659  sotr2  5507  somin2  5997  f1elima  7023  f1imaeq  7025  soisoi  7083  isosolem  7102  xpexr2  7626  smoword  8005  unxpdomlem3  8726  fiming  8964  fiinfg  8965  sornom  9701  fin1a2s  9838  mul4r  10811  mulsub  11085  leltadd  11126  ltord1  11168  leord1  11169  eqord1  11170  divmul24  11346  expcan  13536  ltexp2  13537  bhmafibid2  14828  fsum  15079  fprod  15297  isprm5  16053  ramub  16351  setcinv  17352  grpidpropd  17874  gsumpropd2lem  17891  cmnpropd  18918  gsumcom3  19100  unitpropd  19449  lidl1el  19993  1marepvmarrepid  21186  1marepvsma1  21194  ordtrest2  21814  filuni  22495  haustsms2  22747  blcomps  23005  blcom  23006  metnrmlem3  23471  cnmpopc  23534  icoopnst  23545  icccvx  23556  equivcfil  23904  volcn  24209  dvmptfsum  24574  cxple  25280  cxple3  25286  uhgr2edg  26992  lnosub  28538  chirredlem2  30170  metider  31136  ordtrest2NEW  31168  fsum2dsub  31880  finxpreclem2  34673  fin2so  34881  cover2  34991  filbcmb  35017  isdrngo2  35238  crngohomfo  35286  unichnidl  35311  cdleme50eq  37679  dvhvaddcomN  38234  ismrc  39305  prproropf1olem4  43675