Theorem an4s 578

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 576	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) )
2		an4s.1	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
3	1, 2	sylbi 120	1 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an42s  579  anandis  582  anandirs  583  trin2  4938  fnun  5237  2elresin  5242  f1co  5348  f1oun  5395  f1oco  5398  f1mpt  5680  poxp  6137  tfrlem7  6222  brecop  6527  th3qlem1  6539  oviec  6543  pmss12g  6577  addcmpblnq  7199  mulcmpblnq  7200  mulpipqqs  7205  mulclnq  7208  mulcanenq  7217  distrnqg  7219  mulcmpblnq0  7276  mulcanenq0ec  7277  mulclnq0  7284  nqnq0a  7286  nqnq0m  7287  distrnq0  7291  genipv  7341  genpelvl  7344  genpelvu  7345  genpml  7349  genpmu  7350  genpcdl  7351  genpcuu  7352  genprndl  7353  genprndu  7354  distrlem1prl  7414  distrlem1pru  7415  ltsopr  7428  addcmpblnr  7571  ltsrprg  7579  addclsr  7585  mulclsr  7586  addasssrg  7588  addresr  7669  mulresr  7670  axaddass  7704  axmulass  7705  axdistr  7706  mulgt0  7863  mul4  7918  add4  7947  2addsub  8000  addsubeq4  8001  sub4  8031  muladd  8170  mulsub  8187  add20i  8278  mulge0i  8406  mulap0b  8440  divmuldivap  8496  ltmul12a  8642  zmulcl  9131  uz2mulcl  9429  qaddcl  9454  qmulcl  9456  qreccl  9461  rpaddcl  9494  ge0addcl  9794  ge0xaddcl  9796  expge1  10361  rexanuz  10792  amgm2  10922  iooinsup  11078  mulcn2  11113  dvds2ln  11562  opoe  11628  omoe  11629  opeo  11630  omeo  11631  lcmgcd  11795  lcmdvds  11796  tgcl  12272  innei  12371  txbas  12466  txss12  12474  txbasval  12475  blsscls2  12701  qtopbasss  12729  bj-indind  13301