Theorem ancom2s 649

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 592	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  660  sotr2  5641  somin2  6167  f1elima  7300  f1imaeq  7302  soisoi  7364  isosolem  7383  xpexr2  7959  smoword  8422  unxpdomlem3  9315  fiming  9567  fiinfg  9568  sornom  10346  fin1a2s  10483  mul4r  11459  mulsub  11733  leltadd  11774  ltord1  11816  leord1  11817  eqord1  11818  divmul24  11998  expcan  14219  ltexp2  14220  bhmafibid2  15515  fsum  15768  fprod  15989  isprm5  16754  ramub  17060  setcinv  18157  grpidpropd  18700  gsumpropd2lem  18717  cmnpropd  19833  gsumcom3  20020  unitpropd  20443  lidl1el  21259  1marepvmarrepid  22602  1marepvsma1  22610  ordtrest2  23233  filuni  23914  haustsms2  24166  blcomps  24424  blcom  24425  metnrmlem3  24902  cnmpopc  24974  icoopnst  24988  icccvx  25000  equivcfil  25352  volcn  25660  dvmptfsum  26033  cxple  26755  cxple3  26761  om2noseqlt2  28324  om2noseqf1o  28325  uhgr2edg  29243  lnosub  30791  chirredlem2  32423  metider  33840  ordtrest2NEW  33869  fsum2dsub  34584  finxpreclem2  37356  fin2so  37567  cover2  37675  filbcmb  37700  isdrngo2  37918  crngohomfo  37966  unichnidl  37991  cdleme50eq  40498  dvhvaddcomN  41053  ismrc  42657  prproropf1olem4  47380