Theorem an42s 589

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 588	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 566	1 |- ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) -> ta )

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 depends on definitions:  df-bi 117

This theorem is referenced by:  nnmsucr  6576  ecopoveq  6719  enqdc  7476  addcmpblnq  7482  addpipqqslem  7484  addpipqqs  7485  addclnq  7490  addcomnqg  7496  distrnqg  7502  recexnq  7505  ltdcnq  7512  ltexnqq  7523  enq0enq  7546  enq0sym  7547  enq0breq  7551  addclnq0  7566  distrnq0  7574  mulclsr  7869  axmulass  7988  axdistr  7989  subadd4  8318  mulsub  8475  mgmidmo  13237  tgcl  14569