Theorem an42s 870

Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)

Hypothesis

Ref	Expression
an41r3s.1	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )

Assertion

Ref	Expression
an42s	|- ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) -> ta )

Proof of Theorem an42s

Step	Hyp	Ref	Expression
1		an41r3s.1	. . 3 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
2	1	an4s 869	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 844	1 |- ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) -> ta )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  nnmsucr  7705  ecopoveq  7848  sbthlem9  8078  mulclsr  9905  mulasssr  9911  distrsr  9912  ltsosr  9915  axmulf  9967  axmulass  9978  axdistr  9979  subadd4  10325  mulsub  10473  mgmidmo  17259  tgcl  20773  bwth  21213  pntibndlem2  25280  hosubadd4  28673  fdc  33541  isdrngo2  33757  unichnidl  33830  acongtr  37545