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  6464  ecopoveq  6604  enqdc  7310  addcmpblnq  7316  addpipqqslem  7318  addpipqqs  7319  addclnq  7324  addcomnqg  7330  distrnqg  7336  recexnq  7339  ltdcnq  7346  ltexnqq  7357  enq0enq  7380  enq0sym  7381  enq0breq  7385  addclnq0  7400  distrnq0  7408  mulclsr  7703  axmulass  7822  axdistr  7823  subadd4  8150  mulsub  8307  mgmidmo  12612  tgcl  12779