Theorem ancom2s 800

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

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  an42s  824  sotr2  4822  somin2  5396  f1elima  6150  f1imaeq  6152  soisoi  6203  isosolem  6222  xpexr2  6715  2ndconst  6862  smoword  7027  unxpdomlem3  7716  sornom  8646  fin1a2s  8783  mulsub  9988  leltadd  10025  ltord1  10068  leord1  10069  eqord1  10070  divmul24  10237  expcan  12173  ltexp2  12174  fsum  13491  isprm5  14101  ramub  14379  setcinv  15264  grpidpropd  15753  gsumpropd2lem  15811  cmnpropd  16596  unitpropd  17123  lidl1el  17641  gsumcom3  18661  1marepvmarrepid  18837  1marepvsma1  18845  ordtrest2  19464  filuni  20114  haustsms2  20363  blcomps  20624  blcom  20625  metnrmlem3  21093  cnmpt2pc  21156  icoopnst  21167  icccvx  21178  equivcfil  21466  volcn  21743  dvmptfsum  22104  cxple  22797  cxple3  22803  subgoablo  24975  ghablo  25033  lnosub  25336  chirredlem2  26972  metider  27495  ordtrest2NEW  27527  fprod  28636  fin2so  29603  cover2  29794  filbcmb  29821  isdrngo2  29951  crngohomfo  29993  unichnidl  30018  ismrc  30224  cdleme50eq  35212  dvhvaddcomN  35768