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  823  sotr2  4668  somin2  5234  f1elima  5974  f1imaeq  5976  soisoi  6017  isosolem  6036  xpexr2  6517  2ndconst  6660  smoword  6825  unxpdomlem3  7517  sornom  8444  fin1a2s  8581  mulsub  9785  leltadd  9821  ltord1  9864  leord1  9865  eqord1  9866  divmul24  10033  expcan  11914  ltexp2  11915  fsum  13195  isprm5  13796  ramub  14072  setcinv  14956  grpidpropd  15445  gsumpropd2lem  15503  cmnpropd  16284  unitpropd  16787  lidl1el  17298  gsumcom3  18297  1marepvmarrepid  18384  1marepvsma1  18392  ordtrest2  18806  filuni  19456  haustsms2  19705  blcomps  19966  blcom  19967  metnrmlem3  20435  cnmpt2pc  20498  icoopnst  20509  icccvx  20520  equivcfil  20808  volcn  21084  dvmptfsum  21445  cxple  22138  cxple3  22144  subgoablo  23796  ghablo  23854  lnosub  24157  chirredlem2  25793  metider  26319  ordtrest2NEW  26351  fprod  27452  fin2so  28413  cover2  28604  filbcmb  28631  isdrngo2  28761  crngohomfo  28803  unichnidl  28828  ismrc  29034  cdleme50eq  34182  dvhvaddcomN  34738