Theorem ancom2s 809

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 450	. 2 |- ( ( ch /\ ps ) -> ( ps /\ ch ) )
2		an12s.1	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	1, 2	sylan2 476	1 |- ( ( ph /\ ( ch /\ ps ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  an42s  834  sotr2  4803  somin2  5254  f1elima  6180  f1imaeq  6182  soisoi  6235  isosolem  6254  xpexr2  6749  2ndconst  6897  smoword  7097  unxpdomlem3  7788  fiming  8024  fiinfg  8025  sornom  8715  fin1a2s  8852  mulsub  10069  leltadd  10106  ltord1  10148  leord1  10149  eqord1  10150  divmul24  10319  expcan  12332  ltexp2  12333  fsum  13786  fprod  13995  isprm5  14651  ramub  14970  setcinv  15985  grpidpropd  16504  gsumpropd2lem  16516  cmnpropd  17439  unitpropd  17925  lidl1el  18442  gsumcom3  19423  1marepvmarrepid  19599  1marepvsma1  19607  ordtrest2  20219  filuni  20899  haustsms2  21150  blcomps  21407  blcom  21408  metnrmlem3  21877  metnrmlem3OLD  21892  cnmpt2pc  21955  icoopnst  21966  icccvx  21977  equivcfil  22268  volcn  22563  dvmptfsum  22926  cxple  23639  cxple3  23645  subgoablo  26038  ghabloOLD  26096  lnosub  26399  chirredlem2  28043  bhmafibid2  28414  metider  28706  ordtrest2NEW  28738  finxpreclem2  31747  fin2so  31897  cover2  32005  filbcmb  32032  isdrngo2  32162  crngohomfo  32204  unichnidl  32229  cdleme50eq  34078  dvhvaddcomN  34634  ismrc  35513  usgr2edg  39098