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  591  ordsuc  4652  xpexr2m  5166  f1elima  5890  f1imaeq  5892  isosolem  5941  caovlem2d  6189  2ndconst  6358  isotilem  7161  prarloclem4  7673  mulsub  8535  leltadd  8582  eqord1  8618  divmul24ap  8851  fprodseq  12080  grpidpropdg  13393  cmnpropd  13818  unitpropdg  14097  blcomps  15055  blcom  15056  dvmptfsum  15384  cxple  15576  cxple3  15580  uhgr2edg  15989