Theorem an4s 592

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 588	. 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  593  anandis  596  anandirs  597  trin2  5154  fnun  5464  2elresin  5469  f1co  5585  f1oun  5634  f1oco  5637  f1mpt  5944  poxp  6428  tfrlem7  6548  brecop  6859  th3qlem1  6871  oviec  6875  pmss12g  6909  addcmpblnq  7682  mulcmpblnq  7683  mulpipqqs  7688  mulclnq  7691  mulcanenq  7700  distrnqg  7702  mulcmpblnq0  7759  mulcanenq0ec  7760  mulclnq0  7767  nqnq0a  7769  nqnq0m  7770  distrnq0  7774  genipv  7824  genpelvl  7827  genpelvu  7828  genpml  7832  genpmu  7833  genpcdl  7834  genpcuu  7835  genprndl  7836  genprndu  7837  distrlem1prl  7897  distrlem1pru  7898  ltsopr  7911  addcmpblnr  8054  ltsrprg  8062  addclsr  8068  mulclsr  8069  addasssrg  8071  addresr  8152  mulresr  8153  axaddass  8187  axmulass  8188  axdistr  8189  mulgt0  8348  mul4  8405  add4  8434  2addsub  8487  addsubeq4  8488  sub4  8518  muladd  8657  mulsub  8674  add20i  8766  mulge0i  8894  mulap0b  8929  divmuldivap  8986  ltmul12a  9134  zmulcl  9631  uz2mulcl  9940  qaddcl  9967  qmulcl  9969  qreccl  9974  rpaddcl  10010  ge0addcl  10314  ge0xaddcl  10316  expge1  10938  rexanuz  11673  amgm2  11803  iooinsup  11962  mulcn2  11997  dvds2ln  12510  opoe  12581  omoe  12582  opeo  12583  omeo  12584  lcmgcd  12775  lcmdvds  12776  pc2dvds  13028  tgcl  14929  innei  15028  txbas  15123  txss12  15131  txbasval  15132  blsscls2  15358  qtopbasss  15386  lgslem3  15875  bj-indind  16702