Theorem an42s 593

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 592	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 568	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  6699  ecopoveq  6842  enqdc  7641  addcmpblnq  7647  addpipqqslem  7649  addpipqqs  7650  addclnq  7655  addcomnqg  7661  distrnqg  7667  recexnq  7670  ltdcnq  7677  ltexnqq  7688  enq0enq  7711  enq0sym  7712  enq0breq  7716  addclnq0  7731  distrnq0  7739  mulclsr  8034  axmulass  8153  axdistr  8154  subadd4  8482  mulsub  8639  mgmidmo  13535  tgcl  14875