Theorem an42s 589

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 588	. 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  6543  ecopoveq  6686  enqdc  7423  addcmpblnq  7429  addpipqqslem  7431  addpipqqs  7432  addclnq  7437  addcomnqg  7443  distrnqg  7449  recexnq  7452  ltdcnq  7459  ltexnqq  7470  enq0enq  7493  enq0sym  7494  enq0breq  7498  addclnq0  7513  distrnq0  7521  mulclsr  7816  axmulass  7935  axdistr  7936  subadd4  8265  mulsub  8422  mgmidmo  12958  tgcl  14243