Theorem an42s 556

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  nnmsucr  6241  ecopoveq  6377  enqdc  6910  addcmpblnq  6916  addpipqqslem  6918  addpipqqs  6919  addclnq  6924  addcomnqg  6930  distrnqg  6936  recexnq  6939  ltdcnq  6946  ltexnqq  6957  enq0enq  6980  enq0sym  6981  enq0breq  6985  addclnq0  7000  distrnq0  7008  mulclsr  7290  axmulass  7398  axdistr  7399  subadd4  7716  mulsub  7869