Theorem an42s 578

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 577	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 555	1 |- ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) -> ta )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnmsucr  6384  ecopoveq  6524  enqdc  7169  addcmpblnq  7175  addpipqqslem  7177  addpipqqs  7178  addclnq  7183  addcomnqg  7189  distrnqg  7195  recexnq  7198  ltdcnq  7205  ltexnqq  7216  enq0enq  7239  enq0sym  7240  enq0breq  7244  addclnq0  7259  distrnq0  7267  mulclsr  7562  axmulass  7681  axdistr  7682  subadd4  8006  mulsub  8163  tgcl  12233