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  5565  somin2  6088  f1elima  7204  f1imaeq  7206  soisoi  7269  isosolem  7288  xpexr2  7859  smoword  8296  unxpdomlem3  9157  fiming  9409  fiinfg  9410  sornom  10190  fin1a2s  10327  mul4r  11303  mulsub  11581  leltadd  11622  ltord1  11664  leord1  11665  eqord1  11666  divmul24  11846  expcan  14094  ltexp2  14095  bhmafibid2  15394  fsum  15645  fprod  15866  isprm5  16636  ramub  16943  setcinv  18015  grpidpropd  18554  gsumpropd2lem  18571  cmnpropd  19688  gsumcom3  19875  unitpropd  20320  lidl1el  21151  1marepvmarrepid  22478  1marepvsma1  22486  ordtrest2  23107  filuni  23788  haustsms2  24040  blcomps  24297  blcom  24298  metnrmlem3  24766  cnmpopc  24838  icoopnst  24852  icccvx  24864  equivcfil  25215  volcn  25523  dvmptfsum  25895  cxple  26620  cxple3  26626  om2noseqlt2  28217  om2noseqf1o  28218  uhgr2edg  29171  lnosub  30721  chirredlem2  32353  metider  33860  ordtrest2NEW  33889  fsum2dsub  34574  finxpreclem2  37363  fin2so  37586  cover2  37694  filbcmb  37719  isdrngo2  37937  crngohomfo  37985  unichnidl  38010  cdleme50eq  40520  dvhvaddcomN  41075  ismrc  42674  prproropf1olem4  47491  pgnbgreunbgrlem4  48093