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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  an42s  660  sotr2  5477  somin2  5971  f1elima  7018  f1imaeq  7020  soisoi  7080  isosolem  7099  xpexr2  7634  smoword  8018  unxpdomlem3  8767  fiming  9000  fiinfg  9001  sornom  9742  fin1a2s  9879  mul4r  10852  mulsub  11126  leltadd  11167  ltord1  11209  leord1  11210  eqord1  11211  divmul24  11387  expcan  13588  ltexp2  13589  bhmafibid2  14879  fsum  15130  fprod  15348  isprm5  16108  ramub  16409  setcinv  17421  grpidpropd  17943  gsumpropd2lem  17960  cmnpropd  18988  gsumcom3  19171  unitpropd  19523  lidl1el  20064  1marepvmarrepid  21280  1marepvsma1  21288  ordtrest2  21909  filuni  22590  haustsms2  22842  blcomps  23100  blcom  23101  metnrmlem3  23567  cnmpopc  23634  icoopnst  23645  icccvx  23656  equivcfil  24004  volcn  24311  dvmptfsum  24679  cxple  25390  cxple3  25396  uhgr2edg  27102  lnosub  28646  chirredlem2  30278  metider  31369  ordtrest2NEW  31398  fsum2dsub  32110  finxpreclem2  35113  fin2so  35350  cover2  35458  filbcmb  35484  isdrngo2  35702  crngohomfo  35750  unichnidl  35775  cdleme50eq  38143  dvhvaddcomN  38698  ismrc  40043  prproropf1olem4  44419