Theorem ancom2s 844

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	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
ancom2s	|- ( ( ph /\ ( ch /\ ps ) ) -> th )

Proof of Theorem ancom2s

Step	Hyp	Ref	Expression
1		pm3.22 465	. 2 |- ( ( ch /\ ps ) -> ( ps /\ ch ) )
2		an12s.1	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	1, 2	sylan2 491	1 |- ( ( ph /\ ( ch /\ ps ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  an42s  870  sotr2  5064  somin2  5531  f1elima  6520  f1imaeq  6522  soisoi  6578  isosolem  6597  xpexr2  7107  2ndconst  7266  smoword  7463  unxpdomlem3  8166  fiming  8404  fiinfg  8405  sornom  9099  fin1a2s  9236  mulsub  10473  leltadd  10512  ltord1  10554  leord1  10555  eqord1  10556  divmul24  10729  expcan  12913  ltexp2  12914  fsum  14451  fprod  14671  isprm5  15419  ramub  15717  setcinv  16740  grpidpropd  17261  gsumpropd2lem  17273  cmnpropd  18202  unitpropd  18697  lidl1el  19218  gsumcom3  20205  1marepvmarrepid  20381  1marepvsma1  20389  ordtrest2  21008  filuni  21689  haustsms2  21940  blcomps  22198  blcom  22199  metnrmlem3  22664  cnmpt2pc  22727  icoopnst  22738  icccvx  22749  equivcfil  23097  volcn  23374  dvmptfsum  23738  cxple  24441  cxple3  24447  uhgr2edg  26100  lnosub  27614  chirredlem2  29250  bhmafibid2  29645  metider  29937  ordtrest2NEW  29969  fsum2dsub  30685  finxpreclem2  33227  fin2so  33396  cover2  33508  filbcmb  33535  isdrngo2  33757  crngohomfo  33805  unichnidl  33830  cdleme50eq  35829  dvhvaddcomN  36385  ismrc  37264