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  5128  fnun  5438  2elresin  5443  f1co  5554  f1oun  5603  f1oco  5606  f1mpt  5912  poxp  6397  tfrlem7  6483  brecop  6794  th3qlem1  6806  oviec  6810  pmss12g  6844  addcmpblnq  7587  mulcmpblnq  7588  mulpipqqs  7593  mulclnq  7596  mulcanenq  7605  distrnqg  7607  mulcmpblnq0  7664  mulcanenq0ec  7665  mulclnq0  7672  nqnq0a  7674  nqnq0m  7675  distrnq0  7679  genipv  7729  genpelvl  7732  genpelvu  7733  genpml  7737  genpmu  7738  genpcdl  7739  genpcuu  7740  genprndl  7741  genprndu  7742  distrlem1prl  7802  distrlem1pru  7803  ltsopr  7816  addcmpblnr  7959  ltsrprg  7967  addclsr  7973  mulclsr  7974  addasssrg  7976  addresr  8057  mulresr  8058  axaddass  8092  axmulass  8093  axdistr  8094  mulgt0  8254  mul4  8311  add4  8340  2addsub  8393  addsubeq4  8394  sub4  8424  muladd  8563  mulsub  8580  add20i  8672  mulge0i  8800  mulap0b  8835  divmuldivap  8892  ltmul12a  9040  zmulcl  9533  uz2mulcl  9842  qaddcl  9869  qmulcl  9871  qreccl  9876  rpaddcl  9912  ge0addcl  10216  ge0xaddcl  10218  expge1  10839  rexanuz  11566  amgm2  11696  iooinsup  11855  mulcn2  11890  dvds2ln  12403  opoe  12474  omoe  12475  opeo  12476  omeo  12477  lcmgcd  12668  lcmdvds  12669  pc2dvds  12921  tgcl  14807  innei  14906  txbas  15001  txss12  15009  txbasval  15010  blsscls2  15236  qtopbasss  15264  lgslem3  15750  bj-indind  16578