Theorem an42s 593

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 592	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 568	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  6721  ecopoveq  6864  enqdc  7676  addcmpblnq  7682  addpipqqslem  7684  addpipqqs  7685  addclnq  7690  addcomnqg  7696  distrnqg  7702  recexnq  7705  ltdcnq  7712  ltexnqq  7723  enq0enq  7746  enq0sym  7747  enq0breq  7751  addclnq0  7766  distrnq0  7774  mulclsr  8069  axmulass  8188  axdistr  8189  subadd4  8517  mulsub  8674  mgmidmo  13585  tgcl  14929