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  6491  ecopoveq  6632  enqdc  7362  addcmpblnq  7368  addpipqqslem  7370  addpipqqs  7371  addclnq  7376  addcomnqg  7382  distrnqg  7388  recexnq  7391  ltdcnq  7398  ltexnqq  7409  enq0enq  7432  enq0sym  7433  enq0breq  7437  addclnq0  7452  distrnq0  7460  mulclsr  7755  axmulass  7874  axdistr  7875  subadd4  8203  mulsub  8360  mgmidmo  12796  tgcl  13649