Theorem an42s 593

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 592	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 568	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  6734  ecopoveq  6877  enqdc  7692  addcmpblnq  7698  addpipqqslem  7700  addpipqqs  7701  addclnq  7706  addcomnqg  7712  distrnqg  7718  recexnq  7721  ltdcnq  7728  ltexnqq  7739  enq0enq  7762  enq0sym  7763  enq0breq  7767  addclnq0  7782  distrnq0  7790  mulclsr  8085  axmulass  8204  axdistr  8205  subadd4  8533  mulsub  8691  mgmidmo  13635  tgcl  15055