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  4595  xpexr2m  5107  f1elima  5816  f1imaeq  5818  isosolem  5867  caovlem2d  6111  2ndconst  6275  isotilem  7065  prarloclem4  7558  mulsub  8420  leltadd  8466  eqord1  8502  divmul24ap  8735  fprodseq  11726  grpidpropdg  12957  cmnpropd  13365  unitpropdg  13644  blcomps  14564  blcom  14565  cxple  15051  cxple3  15055