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  4660  xpexr2m  5177  f1elima  5916  f1imaeq  5918  isosolem  5967  caovlem2d  6217  2ndconst  6389  isotilem  7207  prarloclem4  7720  mulsub  8582  leltadd  8629  eqord1  8665  divmul24ap  8898  fprodseq  12164  grpidpropdg  13477  cmnpropd  13902  unitpropdg  14183  blcomps  15146  blcom  15147  dvmptfsum  15475  cxple  15667  cxple3  15671  uhgr2edg  16083