Theorem an42s 584

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 583	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 561	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  6467  ecopoveq  6608  enqdc  7323  addcmpblnq  7329  addpipqqslem  7331  addpipqqs  7332  addclnq  7337  addcomnqg  7343  distrnqg  7349  recexnq  7352  ltdcnq  7359  ltexnqq  7370  enq0enq  7393  enq0sym  7394  enq0breq  7398  addclnq0  7413  distrnq0  7421  mulclsr  7716  axmulass  7835  axdistr  7836  subadd4  8163  mulsub  8320  mgmidmo  12626  tgcl  12858