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  4661  xpexr2m  5178  f1elima  5913  f1imaeq  5915  isosolem  5964  caovlem2d  6214  2ndconst  6386  isotilem  7204  prarloclem4  7717  mulsub  8579  leltadd  8626  eqord1  8662  divmul24ap  8895  fprodseq  12143  grpidpropdg  13456  cmnpropd  13881  unitpropdg  14161  blcomps  15119  blcom  15120  dvmptfsum  15448  cxple  15640  cxple3  15644  uhgr2edg  16056