Theorem an42s 597

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 596	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
3	2	ancom2s 572	1 |- ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) -> ta )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  nnmsucr  6761  ecopoveq  6904  enqdc  7729  addcmpblnq  7735  addpipqqslem  7737  addpipqqs  7738  addclnq  7743  addcomnqg  7749  distrnqg  7755  recexnq  7758  ltdcnq  7765  ltexnqq  7776  enq0enq  7799  enq0sym  7800  enq0breq  7804  addclnq0  7819  distrnq0  7827  mulclsr  8122  axmulass  8241  axdistr  8242  subadd4  8572  mulsub  8730  mgmidmo  13743  tgcl  15217