Theorem an4s 590

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  591  anandis  594  anandirs  595  trin2  5120  fnun  5429  2elresin  5434  f1co  5543  f1oun  5592  f1oco  5595  f1mpt  5895  poxp  6378  tfrlem7  6463  brecop  6772  th3qlem1  6784  oviec  6788  pmss12g  6822  addcmpblnq  7554  mulcmpblnq  7555  mulpipqqs  7560  mulclnq  7563  mulcanenq  7572  distrnqg  7574  mulcmpblnq0  7631  mulcanenq0ec  7632  mulclnq0  7639  nqnq0a  7641  nqnq0m  7642  distrnq0  7646  genipv  7696  genpelvl  7699  genpelvu  7700  genpml  7704  genpmu  7705  genpcdl  7706  genpcuu  7707  genprndl  7708  genprndu  7709  distrlem1prl  7769  distrlem1pru  7770  ltsopr  7783  addcmpblnr  7926  ltsrprg  7934  addclsr  7940  mulclsr  7941  addasssrg  7943  addresr  8024  mulresr  8025  axaddass  8059  axmulass  8060  axdistr  8061  mulgt0  8221  mul4  8278  add4  8307  2addsub  8360  addsubeq4  8361  sub4  8391  muladd  8530  mulsub  8547  add20i  8639  mulge0i  8767  mulap0b  8802  divmuldivap  8859  ltmul12a  9007  zmulcl  9500  uz2mulcl  9803  qaddcl  9830  qmulcl  9832  qreccl  9837  rpaddcl  9873  ge0addcl  10177  ge0xaddcl  10179  expge1  10798  rexanuz  11499  amgm2  11629  iooinsup  11788  mulcn2  11823  dvds2ln  12335  opoe  12406  omoe  12407  opeo  12408  omeo  12409  lcmgcd  12600  lcmdvds  12601  pc2dvds  12853  tgcl  14738  innei  14837  txbas  14932  txss12  14940  txbasval  14941  blsscls2  15167  qtopbasss  15195  lgslem3  15681  bj-indind  16295