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  5075  fnun  5383  2elresin  5388  f1co  5495  f1oun  5544  f1oco  5547  f1mpt  5842  poxp  6320  tfrlem7  6405  brecop  6714  th3qlem1  6726  oviec  6730  pmss12g  6764  addcmpblnq  7482  mulcmpblnq  7483  mulpipqqs  7488  mulclnq  7491  mulcanenq  7500  distrnqg  7502  mulcmpblnq0  7559  mulcanenq0ec  7560  mulclnq0  7567  nqnq0a  7569  nqnq0m  7570  distrnq0  7574  genipv  7624  genpelvl  7627  genpelvu  7628  genpml  7632  genpmu  7633  genpcdl  7634  genpcuu  7635  genprndl  7636  genprndu  7637  distrlem1prl  7697  distrlem1pru  7698  ltsopr  7711  addcmpblnr  7854  ltsrprg  7862  addclsr  7868  mulclsr  7869  addasssrg  7871  addresr  7952  mulresr  7953  axaddass  7987  axmulass  7988  axdistr  7989  mulgt0  8149  mul4  8206  add4  8235  2addsub  8288  addsubeq4  8289  sub4  8319  muladd  8458  mulsub  8475  add20i  8567  mulge0i  8695  mulap0b  8730  divmuldivap  8787  ltmul12a  8935  zmulcl  9428  uz2mulcl  9731  qaddcl  9758  qmulcl  9760  qreccl  9765  rpaddcl  9801  ge0addcl  10105  ge0xaddcl  10107  expge1  10723  rexanuz  11332  amgm2  11462  iooinsup  11621  mulcn2  11656  dvds2ln  12168  opoe  12239  omoe  12240  opeo  12241  omeo  12242  lcmgcd  12433  lcmdvds  12434  pc2dvds  12686  tgcl  14569  innei  14668  txbas  14763  txss12  14771  txbasval  14772  blsscls2  14998  qtopbasss  15026  lgslem3  15512  bj-indind  15905