Theorem an42s 523

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

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  nnmsucr  6067  ecopoveq  6201  enqdc  6459  addcmpblnq  6465  addpipqqslem  6467  addpipqqs  6468  addclnq  6473  addcomnqg  6479  distrnqg  6485  recexnq  6488  ltdcnq  6495  ltexnqq  6506  enq0enq  6529  enq0sym  6530  enq0breq  6534  addclnq0  6549  distrnq0  6557  mulclsr  6839  axmulass  6947  axdistr  6948  subadd4  7255  mulsub  7398