Theorem an4s 588

Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)

Hypothesis

Ref	Expression
an4s.1	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )

Assertion

Ref	Expression
an4s	|- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )

Proof of Theorem an4s

Step	Hyp	Ref	Expression
1		an4 586	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) )
2		an4s.1	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
3	1, 2	sylbi 121	1 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> 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:  an42s  589  anandis  592  anandirs  593  trin2  5074  fnun  5382  2elresin  5387  f1co  5493  f1oun  5542  f1oco  5545  f1mpt  5840  poxp  6318  tfrlem7  6403  brecop  6712  th3qlem1  6724  oviec  6728  pmss12g  6762  addcmpblnq  7480  mulcmpblnq  7481  mulpipqqs  7486  mulclnq  7489  mulcanenq  7498  distrnqg  7500  mulcmpblnq0  7557  mulcanenq0ec  7558  mulclnq0  7565  nqnq0a  7567  nqnq0m  7568  distrnq0  7572  genipv  7622  genpelvl  7625  genpelvu  7626  genpml  7630  genpmu  7631  genpcdl  7632  genpcuu  7633  genprndl  7634  genprndu  7635  distrlem1prl  7695  distrlem1pru  7696  ltsopr  7709  addcmpblnr  7852  ltsrprg  7860  addclsr  7866  mulclsr  7867  addasssrg  7869  addresr  7950  mulresr  7951  axaddass  7985  axmulass  7986  axdistr  7987  mulgt0  8147  mul4  8204  add4  8233  2addsub  8286  addsubeq4  8287  sub4  8317  muladd  8456  mulsub  8473  add20i  8565  mulge0i  8693  mulap0b  8728  divmuldivap  8785  ltmul12a  8933  zmulcl  9426  uz2mulcl  9729  qaddcl  9756  qmulcl  9758  qreccl  9763  rpaddcl  9799  ge0addcl  10103  ge0xaddcl  10105  expge1  10721  rexanuz  11299  amgm2  11429  iooinsup  11588  mulcn2  11623  dvds2ln  12135  opoe  12206  omoe  12207  opeo  12208  omeo  12209  lcmgcd  12400  lcmdvds  12401  pc2dvds  12653  tgcl  14536  innei  14635  txbas  14730  txss12  14738  txbasval  14739  blsscls2  14965  qtopbasss  14993  lgslem3  15479  bj-indind  15872