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  6541  ecopoveq  6684  enqdc  7421  addcmpblnq  7427  addpipqqslem  7429  addpipqqs  7430  addclnq  7435  addcomnqg  7441  distrnqg  7447  recexnq  7450  ltdcnq  7457  ltexnqq  7468  enq0enq  7491  enq0sym  7492  enq0breq  7496  addclnq0  7511  distrnq0  7519  mulclsr  7814  axmulass  7933  axdistr  7934  subadd4  8263  mulsub  8420  mgmidmo  12955  tgcl  14232