Theorem an42s 579

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 578	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 556	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  6392  ecopoveq  6532  enqdc  7193  addcmpblnq  7199  addpipqqslem  7201  addpipqqs  7202  addclnq  7207  addcomnqg  7213  distrnqg  7219  recexnq  7222  ltdcnq  7229  ltexnqq  7240  enq0enq  7263  enq0sym  7264  enq0breq  7268  addclnq0  7283  distrnq0  7291  mulclsr  7586  axmulass  7705  axdistr  7706  subadd4  8030  mulsub  8187  tgcl  12272