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  5159  fnun  5469  2elresin  5474  f1co  5590  f1oun  5639  f1oco  5642  f1mpt  5950  poxp  6441  tfrlem7  6561  brecop  6872  th3qlem1  6884  oviec  6888  pmss12g  6922  addcmpblnq  7698  mulcmpblnq  7699  mulpipqqs  7704  mulclnq  7707  mulcanenq  7716  distrnqg  7718  mulcmpblnq0  7775  mulcanenq0ec  7776  mulclnq0  7783  nqnq0a  7785  nqnq0m  7786  distrnq0  7790  genipv  7840  genpelvl  7843  genpelvu  7844  genpml  7848  genpmu  7849  genpcdl  7850  genpcuu  7851  genprndl  7852  genprndu  7853  distrlem1prl  7913  distrlem1pru  7914  ltsopr  7927  addcmpblnr  8070  ltsrprg  8078  addclsr  8084  mulclsr  8085  addasssrg  8087  addresr  8168  mulresr  8169  axaddass  8203  axmulass  8204  axdistr  8205  mulgt0  8364  mul4  8421  add4  8450  2addsub  8503  addsubeq4  8504  sub4  8534  muladd  8674  mulsub  8691  add20i  8783  mulge0i  8911  mulap0b  8946  divmuldivap  9003  ltmul12a  9151  zmulcl  9648  uz2mulcl  9958  qaddcl  9985  qmulcl  9987  qreccl  9992  rpaddcl  10028  ge0addcl  10333  ge0xaddcl  10335  expge1  10962  rexanuz  11698  amgm2  11828  iooinsup  11987  mulcn2  12022  dvds2ln  12535  opoe  12606  omoe  12607  opeo  12608  omeo  12609  lcmgcd  12800  lcmdvds  12801  pc2dvds  13053  tgcl  15055  innei  15154  txbas  15249  txss12  15257  txbasval  15258  blsscls2  15484  qtopbasss  15512  lgslem3  16001  bj-indind  16828