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  5135  fnun  5445  2elresin  5450  f1co  5563  f1oun  5612  f1oco  5615  f1mpt  5922  poxp  6406  tfrlem7  6526  brecop  6837  th3qlem1  6849  oviec  6853  pmss12g  6887  addcmpblnq  7647  mulcmpblnq  7648  mulpipqqs  7653  mulclnq  7656  mulcanenq  7665  distrnqg  7667  mulcmpblnq0  7724  mulcanenq0ec  7725  mulclnq0  7732  nqnq0a  7734  nqnq0m  7735  distrnq0  7739  genipv  7789  genpelvl  7792  genpelvu  7793  genpml  7797  genpmu  7798  genpcdl  7799  genpcuu  7800  genprndl  7801  genprndu  7802  distrlem1prl  7862  distrlem1pru  7863  ltsopr  7876  addcmpblnr  8019  ltsrprg  8027  addclsr  8033  mulclsr  8034  addasssrg  8036  addresr  8117  mulresr  8118  axaddass  8152  axmulass  8153  axdistr  8154  mulgt0  8313  mul4  8370  add4  8399  2addsub  8452  addsubeq4  8453  sub4  8483  muladd  8622  mulsub  8639  add20i  8731  mulge0i  8859  mulap0b  8894  divmuldivap  8951  ltmul12a  9099  zmulcl  9594  uz2mulcl  9903  qaddcl  9930  qmulcl  9932  qreccl  9937  rpaddcl  9973  ge0addcl  10277  ge0xaddcl  10279  expge1  10901  rexanuz  11628  amgm2  11758  iooinsup  11917  mulcn2  11952  dvds2ln  12465  opoe  12536  omoe  12537  opeo  12538  omeo  12539  lcmgcd  12730  lcmdvds  12731  pc2dvds  12983  tgcl  14875  innei  14974  txbas  15069  txss12  15077  txbasval  15078  blsscls2  15304  qtopbasss  15332  lgslem3  15821  bj-indind  16648