Theorem ancom2s 572

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  597  ordsuc  4705  xpexr2m  5224  f1elima  5969  f1imaeq  5971  isosolem  6020  caovlem2d  6272  2ndconst  6448  isotilem  7336  prarloclem4  7855  mulsub  8718  leltadd  8765  eqord1  8801  divmul24ap  9036  fprodseq  12328  grpidpropdg  13671  cmnpropd  14075  unitpropdg  14428  blcomps  15420  blcom  15421  dvmptfsum  15749  cxple  15942  cxple3  15946  uhgr2edg  16361