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  6634  ecopoveq  6777  enqdc  7548  addcmpblnq  7554  addpipqqslem  7556  addpipqqs  7557  addclnq  7562  addcomnqg  7568  distrnqg  7574  recexnq  7577  ltdcnq  7584  ltexnqq  7595  enq0enq  7618  enq0sym  7619  enq0breq  7623  addclnq0  7638  distrnq0  7646  mulclsr  7941  axmulass  8060  axdistr  8061  subadd4  8390  mulsub  8547  mgmidmo  13405  tgcl  14738