Theorem ancom2s 561

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  584  ordsuc  4547  xpexr2m  5052  f1elima  5752  f1imaeq  5754  isosolem  5803  caovlem2d  6045  2ndconst  6201  isotilem  6983  prarloclem4  7460  mulsub  8320  leltadd  8366  eqord1  8402  divmul24ap  8633  fprodseq  11546  grpidpropdg  12628  blcomps  13190  blcom  13191  cxple  13631  cxple3  13635