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  6574  ecopoveq  6717  enqdc  7474  addcmpblnq  7480  addpipqqslem  7482  addpipqqs  7483  addclnq  7488  addcomnqg  7494  distrnqg  7500  recexnq  7503  ltdcnq  7510  ltexnqq  7521  enq0enq  7544  enq0sym  7545  enq0breq  7549  addclnq0  7564  distrnq0  7572  mulclsr  7867  axmulass  7986  axdistr  7987  subadd4  8316  mulsub  8473  mgmidmo  13204  tgcl  14536