Theorem an42s 579

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

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnmsucr  6456  ecopoveq  6596  enqdc  7302  addcmpblnq  7308  addpipqqslem  7310  addpipqqs  7311  addclnq  7316  addcomnqg  7322  distrnqg  7328  recexnq  7331  ltdcnq  7338  ltexnqq  7349  enq0enq  7372  enq0sym  7373  enq0breq  7377  addclnq0  7392  distrnq0  7400  mulclsr  7695  axmulass  7814  axdistr  7815  subadd4  8142  mulsub  8299  mgmidmo  12603  tgcl  12704