Theorem an4s 583

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 581	. 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  584  anandis  587  anandirs  588  trin2  5002  fnun  5304  2elresin  5309  f1co  5415  f1oun  5462  f1oco  5465  f1mpt  5750  poxp  6211  tfrlem7  6296  brecop  6603  th3qlem1  6615  oviec  6619  pmss12g  6653  addcmpblnq  7329  mulcmpblnq  7330  mulpipqqs  7335  mulclnq  7338  mulcanenq  7347  distrnqg  7349  mulcmpblnq0  7406  mulcanenq0ec  7407  mulclnq0  7414  nqnq0a  7416  nqnq0m  7417  distrnq0  7421  genipv  7471  genpelvl  7474  genpelvu  7475  genpml  7479  genpmu  7480  genpcdl  7481  genpcuu  7482  genprndl  7483  genprndu  7484  distrlem1prl  7544  distrlem1pru  7545  ltsopr  7558  addcmpblnr  7701  ltsrprg  7709  addclsr  7715  mulclsr  7716  addasssrg  7718  addresr  7799  mulresr  7800  axaddass  7834  axmulass  7835  axdistr  7836  mulgt0  7994  mul4  8051  add4  8080  2addsub  8133  addsubeq4  8134  sub4  8164  muladd  8303  mulsub  8320  add20i  8411  mulge0i  8539  mulap0b  8573  divmuldivap  8629  ltmul12a  8776  zmulcl  9265  uz2mulcl  9567  qaddcl  9594  qmulcl  9596  qreccl  9601  rpaddcl  9634  ge0addcl  9938  ge0xaddcl  9940  expge1  10513  rexanuz  10952  amgm2  11082  iooinsup  11240  mulcn2  11275  dvds2ln  11786  opoe  11854  omoe  11855  opeo  11856  omeo  11857  lcmgcd  12032  lcmdvds  12033  pc2dvds  12283  tgcl  12858  innei  12957  txbas  13052  txss12  13060  txbasval  13061  blsscls2  13287  qtopbasss  13315  lgslem3  13697  bj-indind  13967