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  5469  somin2  5962  f1elima  6999  f1imaeq  7001  soisoi  7060  isosolem  7079  xpexr2  7606  smoword  7986  unxpdomlem3  8708  fiming  8946  fiinfg  8947  sornom  9688  fin1a2s  9825  mul4r  10798  mulsub  11072  leltadd  11113  ltord1  11155  leord1  11156  eqord1  11157  divmul24  11333  expcan  13529  ltexp2  13530  bhmafibid2  14818  fsum  15069  fprod  15287  isprm5  16041  ramub  16339  setcinv  17342  grpidpropd  17864  gsumpropd2lem  17881  cmnpropd  18908  gsumcom3  19091  unitpropd  19443  lidl1el  19984  1marepvmarrepid  21180  1marepvsma1  21188  ordtrest2  21809  filuni  22490  haustsms2  22742  blcomps  23000  blcom  23001  metnrmlem3  23466  cnmpopc  23533  icoopnst  23544  icccvx  23555  equivcfil  23903  volcn  24210  dvmptfsum  24578  cxple  25286  cxple3  25292  uhgr2edg  26998  lnosub  28542  chirredlem2  30174  metider  31247  ordtrest2NEW  31276  fsum2dsub  31988  finxpreclem2  34807  fin2so  35044  cover2  35152  filbcmb  35178  isdrngo2  35396  crngohomfo  35444  unichnidl  35469  cdleme50eq  37837  dvhvaddcomN  38392  ismrc  39642  prproropf1olem4  44023