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  5556  somin2  6079  f1elima  7192  f1imaeq  7194  soisoi  7257  isosolem  7276  xpexr2  7844  smoword  8281  unxpdomlem3  9137  fiming  9379  fiinfg  9380  sornom  10160  fin1a2s  10297  mul4r  11274  mulsub  11552  leltadd  11593  ltord1  11635  leord1  11636  eqord1  11637  divmul24  11817  expcan  14068  ltexp2  14069  bhmafibid2  15368  fsum  15619  fprod  15840  isprm5  16610  ramub  16917  setcinv  17989  grpidpropd  18562  gsumpropd2lem  18579  cmnpropd  19696  gsumcom3  19883  unitpropd  20328  lidl1el  21156  1marepvmarrepid  22483  1marepvsma1  22491  ordtrest2  23112  filuni  23793  haustsms2  24045  blcomps  24301  blcom  24302  metnrmlem3  24770  cnmpopc  24842  icoopnst  24856  icccvx  24868  equivcfil  25219  volcn  25527  dvmptfsum  25899  cxple  26624  cxple3  26630  om2noseqlt2  28223  om2noseqf1o  28224  uhgr2edg  29179  lnosub  30729  chirredlem2  32361  metider  33897  ordtrest2NEW  33926  fsum2dsub  34610  finxpreclem2  37403  fin2so  37626  cover2  37734  filbcmb  37759  isdrngo2  37977  crngohomfo  38025  unichnidl  38050  cdleme50eq  40559  dvhvaddcomN  41114  ismrc  42713  prproropf1olem4  47516  pgnbgreunbgrlem4  48129