Theorem an42s 578

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 577	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 555	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  6377  ecopoveq  6517  enqdc  7162  addcmpblnq  7168  addpipqqslem  7170  addpipqqs  7171  addclnq  7176  addcomnqg  7182  distrnqg  7188  recexnq  7191  ltdcnq  7198  ltexnqq  7209  enq0enq  7232  enq0sym  7233  enq0breq  7237  addclnq0  7252  distrnq0  7260  mulclsr  7555  axmulass  7674  axdistr  7675  subadd4  7999  mulsub  8156  tgcl  12222