Theorem ancom2s 663

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an42s  674  sotr2  5589  somin2  6123  f1elima  7255  f1imaeq  7257  soisoi  7324  isosolem  7343  xpexr2  7914  smoword  8352  unxpdomlem3  9227  fiming  9470  fiinfg  9471  sornom  10326  fin1a2s  10463  mul4r  11450  mulsub  11728  leltadd  11769  ltord1  11811  leord1  11812  eqord1  11813  divmul24  11990  expcan  14280  ltexp2  14281  bhmafibid2  15603  fsum  15853  fprod  16075  isprm5  16845  ramub  17152  setcinv  18226  grpidpropd  18803  gsumpropd2lem  18829  cmnpropd  19966  gsumcom3  20153  unitpropd  20608  isdrng3lem2  20967  lidl1el  21466  1marepvmarrepid  22851  1marepvsma1  22859  ordtrest2  23483  filuni  24165  haustsms2  24417  blcomps  24673  blcom  24674  metnrmlem3  25142  cnmpopc  25210  icoopnst  25221  icccvx  25232  equivcfil  25581  volcn  25888  dvmptfsum  26256  cxple  26986  cxple3  26992  om2noseqlt2  28619  om2noseqf1o  28620  uhgr2edg  29722  lnosub  31294  chirredlem2  32926  metider  34459  ordtrest2NEW  34488  fsum2dsub  35170  finxpreclem2  38233  fin2so  38450  cover2  38569  filbcmb  38594  isdrngo2  38812  crngohomfo  38860  unichnidl  38885  cdleme50eq  41518  dvhvaddcomN  42073  ismrc  43650  prproropf1olem4  48510  pgnbgreunbgrlem4  49139