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  4599  xpexr2m  5111  f1elima  5820  f1imaeq  5822  isosolem  5871  caovlem2d  6116  2ndconst  6280  isotilem  7072  prarloclem4  7565  mulsub  8427  leltadd  8474  eqord1  8510  divmul24ap  8743  fprodseq  11748  grpidpropdg  13017  cmnpropd  13425  unitpropdg  13704  blcomps  14632  blcom  14633  dvmptfsum  14961  cxple  15153  cxple3  15157