Theorem ancom2s 647

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  an42s  658  sotr2  5535  somin2  6040  f1elima  7136  f1imaeq  7138  soisoi  7199  isosolem  7218  xpexr2  7766  smoword  8197  unxpdomlem3  9029  fiming  9257  fiinfg  9258  sornom  10033  fin1a2s  10170  mul4r  11144  mulsub  11418  leltadd  11459  ltord1  11501  leord1  11502  eqord1  11503  divmul24  11679  expcan  13887  ltexp2  13888  bhmafibid2  15178  fsum  15432  fprod  15651  isprm5  16412  ramub  16714  setcinv  17805  grpidpropd  18346  gsumpropd2lem  18363  cmnpropd  19396  gsumcom3  19579  unitpropd  19939  lidl1el  20489  1marepvmarrepid  21724  1marepvsma1  21732  ordtrest2  22355  filuni  23036  haustsms2  23288  blcomps  23546  blcom  23547  metnrmlem3  24024  cnmpopc  24091  icoopnst  24102  icccvx  24113  equivcfil  24463  volcn  24770  dvmptfsum  25139  cxple  25850  cxple3  25856  uhgr2edg  27575  lnosub  29121  chirredlem2  30753  metider  31844  ordtrest2NEW  31873  fsum2dsub  32587  finxpreclem2  35561  fin2so  35764  cover2  35872  filbcmb  35898  isdrngo2  36116  crngohomfo  36164  unichnidl  36189  cdleme50eq  38555  dvhvaddcomN  39110  ismrc  40523  prproropf1olem4  44958