Theorem ancom2s 556

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 263	. 2 |- ( ( ch /\ ps ) -> ( ps /\ ch ) )
2		an12s.1	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	1, 2	sylan2 284	1 |- ( ( ph /\ ( ch /\ ps ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  an42s  579  ordsuc  4540  xpexr2m  5045  f1elima  5741  f1imaeq  5743  isosolem  5792  caovlem2d  6034  2ndconst  6190  isotilem  6971  prarloclem4  7439  mulsub  8299  leltadd  8345  eqord1  8381  divmul24ap  8612  fprodseq  11524  grpidpropdg  12605  blcomps  13036  blcom  13037  cxple  13477  cxple3  13481