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  5505  somin2  5995  f1elima  7021  f1imaeq  7023  soisoi  7081  isosolem  7100  xpexr2  7624  smoword  8003  unxpdomlem3  8724  fiming  8962  fiinfg  8963  sornom  9699  fin1a2s  9836  mul4r  10809  mulsub  11083  leltadd  11124  ltord1  11166  leord1  11167  eqord1  11168  divmul24  11344  expcan  13534  ltexp2  13535  bhmafibid2  14826  fsum  15077  fprod  15295  isprm5  16051  ramub  16349  setcinv  17350  grpidpropd  17872  gsumpropd2lem  17889  cmnpropd  18916  gsumcom3  19098  unitpropd  19447  lidl1el  19991  1marepvmarrepid  21184  1marepvsma1  21192  ordtrest2  21812  filuni  22493  haustsms2  22745  blcomps  23003  blcom  23004  metnrmlem3  23469  cnmpopc  23532  icoopnst  23543  icccvx  23554  equivcfil  23902  volcn  24207  dvmptfsum  24572  cxple  25278  cxple3  25284  uhgr2edg  26990  lnosub  28536  chirredlem2  30168  metider  31134  ordtrest2NEW  31166  fsum2dsub  31878  finxpreclem2  34674  fin2so  34894  cover2  35004  filbcmb  35030  isdrngo2  35251  crngohomfo  35299  unichnidl  35324  cdleme50eq  37692  dvhvaddcomN  38247  ismrc  39318  prproropf1olem4  43688