Theorem an42s 597

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 596	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 572	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  6751  ecopoveq  6894  enqdc  7718  addcmpblnq  7724  addpipqqslem  7726  addpipqqs  7727  addclnq  7732  addcomnqg  7738  distrnqg  7744  recexnq  7747  ltdcnq  7754  ltexnqq  7765  enq0enq  7788  enq0sym  7789  enq0breq  7793  addclnq0  7808  distrnq0  7816  mulclsr  8111  axmulass  8230  axdistr  8231  subadd4  8560  mulsub  8718  mgmidmo  13669  tgcl  15088