Theorem an42s 591

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 590	. 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  6647  ecopoveq  6790  enqdc  7564  addcmpblnq  7570  addpipqqslem  7572  addpipqqs  7573  addclnq  7578  addcomnqg  7584  distrnqg  7590  recexnq  7593  ltdcnq  7600  ltexnqq  7611  enq0enq  7634  enq0sym  7635  enq0breq  7639  addclnq0  7654  distrnq0  7662  mulclsr  7957  axmulass  8076  axdistr  8077  subadd4  8406  mulsub  8563  mgmidmo  13426  tgcl  14759