Theorem ancom2s 568

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

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  an42s  593  ordsuc  4685  xpexr2m  5204  f1elima  5946  f1imaeq  5948  isosolem  5997  caovlem2d  6247  2ndconst  6418  isotilem  7297  prarloclem4  7813  mulsub  8674  leltadd  8721  eqord1  8757  divmul24ap  8990  fprodseq  12269  grpidpropdg  13587  cmnpropd  14012  unitpropdg  14293  blcomps  15261  blcom  15262  dvmptfsum  15590  cxple  15782  cxple3  15786  uhgr2edg  16201