Theorem ancom2s 650

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 593	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  661  sotr2  5595  somin2  6124  f1elima  7256  f1imaeq  7258  soisoi  7321  isosolem  7340  xpexr2  7915  smoword  8380  unxpdomlem3  9260  fiming  9512  fiinfg  9513  sornom  10291  fin1a2s  10428  mul4r  11404  mulsub  11680  leltadd  11721  ltord1  11763  leord1  11764  eqord1  11765  divmul24  11945  expcan  14187  ltexp2  14188  bhmafibid2  15485  fsum  15736  fprod  15957  isprm5  16726  ramub  17033  setcinv  18103  grpidpropd  18640  gsumpropd2lem  18657  cmnpropd  19772  gsumcom3  19959  unitpropd  20377  lidl1el  21187  1marepvmarrepid  22513  1marepvsma1  22521  ordtrest2  23142  filuni  23823  haustsms2  24075  blcomps  24332  blcom  24333  metnrmlem3  24801  cnmpopc  24873  icoopnst  24887  icccvx  24899  equivcfil  25251  volcn  25559  dvmptfsum  25931  cxple  26656  cxple3  26662  om2noseqlt2  28246  om2noseqf1o  28247  uhgr2edg  29187  lnosub  30740  chirredlem2  32372  metider  33925  ordtrest2NEW  33954  fsum2dsub  34639  finxpreclem2  37408  fin2so  37631  cover2  37739  filbcmb  37764  isdrngo2  37982  crngohomfo  38030  unichnidl  38055  cdleme50eq  40560  dvhvaddcomN  41115  ismrc  42724  prproropf1olem4  47520