Theorem ancom2s 861

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  an42s  887  sotr2  5093  somin2  5566  f1elima  6560  f1imaeq  6562  soisoi  6618  isosolem  6637  xpexr2  7149  2ndconst  7311  smoword  7508  unxpdomlem3  8207  fiming  8445  fiinfg  8446  sornom  9137  fin1a2s  9274  mulsub  10511  leltadd  10550  ltord1  10592  leord1  10593  eqord1  10594  divmul24  10767  expcan  12953  ltexp2  12954  fsum  14495  fprod  14715  isprm5  15466  ramub  15764  setcinv  16787  grpidpropd  17308  gsumpropd2lem  17320  cmnpropd  18248  unitpropd  18743  lidl1el  19266  gsumcom3  20253  1marepvmarrepid  20429  1marepvsma1  20437  ordtrest2  21056  filuni  21736  haustsms2  21987  blcomps  22245  blcom  22246  metnrmlem3  22711  cnmpt2pc  22774  icoopnst  22785  icccvx  22796  equivcfil  23143  volcn  23420  dvmptfsum  23783  cxple  24486  cxple3  24492  uhgr2edg  26145  lnosub  27742  chirredlem2  29378  bhmafibid2  29773  metider  30065  ordtrest2NEW  30097  fsum2dsub  30813  finxpreclem2  33357  fin2so  33526  cover2  33638  filbcmb  33665  isdrngo2  33887  crngohomfo  33935  unichnidl  33960  cdleme50eq  36146  dvhvaddcomN  36702  ismrc  37581