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  4995  fnun  5294  2elresin  5299  f1co  5405  f1oun  5452  f1oco  5455  f1mpt  5739  poxp  6200  tfrlem7  6285  brecop  6591  th3qlem1  6603  oviec  6607  pmss12g  6641  addcmpblnq  7308  mulcmpblnq  7309  mulpipqqs  7314  mulclnq  7317  mulcanenq  7326  distrnqg  7328  mulcmpblnq0  7385  mulcanenq0ec  7386  mulclnq0  7393  nqnq0a  7395  nqnq0m  7396  distrnq0  7400  genipv  7450  genpelvl  7453  genpelvu  7454  genpml  7458  genpmu  7459  genpcdl  7460  genpcuu  7461  genprndl  7462  genprndu  7463  distrlem1prl  7523  distrlem1pru  7524  ltsopr  7537  addcmpblnr  7680  ltsrprg  7688  addclsr  7694  mulclsr  7695  addasssrg  7697  addresr  7778  mulresr  7779  axaddass  7813  axmulass  7814  axdistr  7815  mulgt0  7973  mul4  8030  add4  8059  2addsub  8112  addsubeq4  8113  sub4  8143  muladd  8282  mulsub  8299  add20i  8390  mulge0i  8518  mulap0b  8552  divmuldivap  8608  ltmul12a  8755  zmulcl  9244  uz2mulcl  9546  qaddcl  9573  qmulcl  9575  qreccl  9580  rpaddcl  9613  ge0addcl  9917  ge0xaddcl  9919  expge1  10492  rexanuz  10930  amgm2  11060  iooinsup  11218  mulcn2  11253  dvds2ln  11764  opoe  11832  omoe  11833  opeo  11834  omeo  11835  lcmgcd  12010  lcmdvds  12011  pc2dvds  12261  tgcl  12704  innei  12803  txbas  12898  txss12  12906  txbasval  12907  blsscls2  13133  qtopbasss  13161  lgslem3  13543  bj-indind  13814