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  4667  xpexr2m  5185  f1elima  5924  f1imaeq  5926  isosolem  5975  caovlem2d  6225  2ndconst  6396  isotilem  7248  prarloclem4  7761  mulsub  8622  leltadd  8669  eqord1  8705  divmul24ap  8938  fprodseq  12207  grpidpropdg  13520  cmnpropd  13945  unitpropdg  14226  blcomps  15190  blcom  15191  dvmptfsum  15519  cxple  15711  cxple3  15715  uhgr2edg  16130