Theorem ancom2s 566

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  589  ordsuc  4615  xpexr2m  5129  f1elima  5849  f1imaeq  5851  isosolem  5900  caovlem2d  6146  2ndconst  6315  isotilem  7115  prarloclem4  7618  mulsub  8480  leltadd  8527  eqord1  8563  divmul24ap  8796  fprodseq  11938  grpidpropdg  13250  cmnpropd  13675  unitpropdg  13954  blcomps  14912  blcom  14913  dvmptfsum  15241  cxple  15433  cxple3  15437