Theorem ancom2s 840

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

This theorem is referenced by:  an42s  866  sotr2  4988  somin2  5450  f1elima  6421  f1imaeq  6423  soisoi  6478  isosolem  6497  xpexr2  7000  2ndconst  7153  smoword  7350  unxpdomlem3  8051  fiming  8287  fiinfg  8288  sornom  8982  fin1a2s  9119  mulsub  10352  leltadd  10391  ltord1  10433  leord1  10434  eqord1  10435  divmul24  10608  expcan  12775  ltexp2  12776  fsum  14298  fprod  14510  isprm5  15257  ramub  15555  setcinv  16563  grpidpropd  17084  gsumpropd2lem  17096  cmnpropd  18025  unitpropd  18520  lidl1el  19039  gsumcom3  20024  1marepvmarrepid  20200  1marepvsma1  20208  ordtrest2  20818  filuni  21499  haustsms2  21750  blcomps  22008  blcom  22009  metnrmlem3  22472  cnmpt2pc  22535  icoopnst  22546  icccvx  22557  equivcfil  22905  volcn  23180  dvmptfsum  23542  cxple  24241  cxple3  24247  lnosub  26998  chirredlem2  28634  bhmafibid2  28976  metider  29265  ordtrest2NEW  29297  finxpreclem2  32403  fin2so  32566  cover2  32678  filbcmb  32705  isdrngo2  32927  crngohomfo  32975  unichnidl  33000  cdleme50eq  34847  dvhvaddcomN  35403  ismrc  36282  uhgr2edg  40435