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  6597  ecopoveq  6740  enqdc  7509  addcmpblnq  7515  addpipqqslem  7517  addpipqqs  7518  addclnq  7523  addcomnqg  7529  distrnqg  7535  recexnq  7538  ltdcnq  7545  ltexnqq  7556  enq0enq  7579  enq0sym  7580  enq0breq  7584  addclnq0  7599  distrnq0  7607  mulclsr  7902  axmulass  8021  axdistr  8022  subadd4  8351  mulsub  8508  mgmidmo  13319  tgcl  14651