Theorem ancom2s 651

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 594	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  662  sotr2  5562  somin2  6087  f1elima  7207  f1imaeq  7209  soisoi  7272  isosolem  7291  xpexr2  7859  smoword  8295  unxpdomlem3  9157  fiming  9402  fiinfg  9403  sornom  10188  fin1a2s  10325  mul4r  11304  mulsub  11582  leltadd  11623  ltord1  11665  leord1  11666  eqord1  11667  divmul24  11848  expcan  14120  ltexp2  14121  bhmafibid2  15420  fsum  15671  fprod  15895  isprm5  16666  ramub  16973  setcinv  18046  grpidpropd  18619  gsumpropd2lem  18636  cmnpropd  19755  gsumcom3  19942  unitpropd  20386  lidl1el  21213  1marepvmarrepid  22528  1marepvsma1  22536  ordtrest2  23157  filuni  23838  haustsms2  24090  blcomps  24346  blcom  24347  metnrmlem3  24815  cnmpopc  24883  icoopnst  24894  icccvx  24905  equivcfil  25254  volcn  25561  dvmptfsum  25930  cxple  26647  cxple3  26653  om2noseqlt2  28280  om2noseqf1o  28281  uhgr2edg  29265  lnosub  30818  chirredlem2  32450  metider  34026  ordtrest2NEW  34055  fsum2dsub  34739  mh-inf3f1  36711  finxpreclem2  37694  fin2so  37916  cover2  38024  filbcmb  38049  isdrngo2  38267  crngohomfo  38315  unichnidl  38340  cdleme50eq  40975  dvhvaddcomN  41530  ismrc  43121  prproropf1olem4  47954  pgnbgreunbgrlem4  48583