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  5626  somin2  6155  f1elima  7283  f1imaeq  7285  soisoi  7348  isosolem  7367  xpexr2  7941  smoword  8406  unxpdomlem3  9288  fiming  9538  fiinfg  9539  sornom  10317  fin1a2s  10454  mul4r  11430  mulsub  11706  leltadd  11747  ltord1  11789  leord1  11790  eqord1  11791  divmul24  11971  expcan  14209  ltexp2  14210  bhmafibid2  15505  fsum  15756  fprod  15977  isprm5  16744  ramub  17051  setcinv  18135  grpidpropd  18675  gsumpropd2lem  18692  cmnpropd  19809  gsumcom3  19996  unitpropd  20417  lidl1el  21236  1marepvmarrepid  22581  1marepvsma1  22589  ordtrest2  23212  filuni  23893  haustsms2  24145  blcomps  24403  blcom  24404  metnrmlem3  24883  cnmpopc  24955  icoopnst  24969  icccvx  24981  equivcfil  25333  volcn  25641  dvmptfsum  26013  cxple  26737  cxple3  26743  om2noseqlt2  28306  om2noseqf1o  28307  uhgr2edg  29225  lnosub  30778  chirredlem2  32410  metider  33893  ordtrest2NEW  33922  fsum2dsub  34622  finxpreclem2  37391  fin2so  37614  cover2  37722  filbcmb  37747  isdrngo2  37965  crngohomfo  38013  unichnidl  38038  cdleme50eq  40543  dvhvaddcomN  41098  ismrc  42712  prproropf1olem4  47493