Theorem ancom2s 658

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 601	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  669  sotr2  5578  somin2  6108  f1elima  7232  f1imaeq  7234  soisoi  7297  isosolem  7316  xpexr2  7885  smoword  8321  unxpdomlem3  9187  fiming  9432  fiinfg  9433  sornom  10220  fin1a2s  10357  mul4r  11338  mulsub  11616  leltadd  11657  ltord1  11699  leord1  11700  eqord1  11701  divmul24  11881  expcan  14168  ltexp2  14169  bhmafibid2  15468  fsum  15719  fprod  15943  isprm5  16714  ramub  17021  setcinv  18095  grpidpropd  18668  gsumpropd2lem  18685  cmnpropd  19803  gsumcom3  19990  unitpropd  20434  lidl1el  21265  1marepvmarrepid  22604  1marepvsma1  22612  ordtrest2  23233  filuni  23914  haustsms2  24166  blcomps  24422  blcom  24423  metnrmlem3  24891  cnmpopc  24959  icoopnst  24970  icccvx  24981  equivcfil  25330  volcn  25637  dvmptfsum  26006  cxple  26726  cxple3  26732  om2noseqlt2  28359  om2noseqf1o  28360  uhgr2edg  29344  lnosub  30897  chirredlem2  32529  metider  34135  ordtrest2NEW  34164  fsum2dsub  34848  mh-inf3f1  36839  finxpreclem2  37822  fin2so  38044  cover2  38152  filbcmb  38177  isdrngo2  38395  crngohomfo  38443  unichnidl  38468  cdleme50eq  41103  dvhvaddcomN  41658  ismrc  43220  prproropf1olem4  48050  pgnbgreunbgrlem4  48679