Theorem ancom2s 816

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  an42s  841  sotr2  4802  somin2  5253  f1elima  6188  f1imaeq  6190  soisoi  6243  isosolem  6262  xpexr2  6760  2ndconst  6911  smoword  7110  unxpdomlem3  7803  fiming  8039  fiinfg  8040  sornom  8732  fin1a2s  8869  mulsub  10088  leltadd  10125  ltord1  10167  leord1  10168  eqord1  10169  divmul24  10338  expcan  12356  ltexp2  12357  fsum  13834  fprod  14043  isprm5  14699  ramub  15018  setcinv  16033  grpidpropd  16552  gsumpropd2lem  16564  cmnpropd  17487  unitpropd  17973  lidl1el  18490  gsumcom3  19472  1marepvmarrepid  19648  1marepvsma1  19656  ordtrest2  20268  filuni  20948  haustsms2  21199  blcomps  21456  blcom  21457  metnrmlem3  21926  metnrmlem3OLD  21941  cnmpt2pc  22004  icoopnst  22015  icccvx  22026  equivcfil  22317  volcn  22612  dvmptfsum  22975  cxple  23688  cxple3  23694  subgoablo  26087  ghabloOLD  26145  lnosub  26448  chirredlem2  28092  bhmafibid2  28454  metider  28745  ordtrest2NEW  28777  finxpreclem2  31826  fin2so  31976  cover2  32084  filbcmb  32111  isdrngo2  32241  crngohomfo  32283  unichnidl  32308  cdleme50eq  34152  dvhvaddcomN  34708  ismrc  35587  uhgr2edg  39338