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  6503  ecopoveq  6644  enqdc  7374  addcmpblnq  7380  addpipqqslem  7382  addpipqqs  7383  addclnq  7388  addcomnqg  7394  distrnqg  7400  recexnq  7403  ltdcnq  7410  ltexnqq  7421  enq0enq  7444  enq0sym  7445  enq0breq  7449  addclnq0  7464  distrnq0  7472  mulclsr  7767  axmulass  7886  axdistr  7887  subadd4  8215  mulsub  8372  mgmidmo  12810  tgcl  13860