Theorem an4s 577

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 575	. 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  578  anandis  581  anandirs  582  trin2  4930  fnun  5229  2elresin  5234  f1co  5340  f1oun  5387  f1oco  5390  f1mpt  5672  poxp  6129  tfrlem7  6214  brecop  6519  th3qlem1  6531  oviec  6535  pmss12g  6569  addcmpblnq  7175  mulcmpblnq  7176  mulpipqqs  7181  mulclnq  7184  mulcanenq  7193  distrnqg  7195  mulcmpblnq0  7252  mulcanenq0ec  7253  mulclnq0  7260  nqnq0a  7262  nqnq0m  7263  distrnq0  7267  genipv  7317  genpelvl  7320  genpelvu  7321  genpml  7325  genpmu  7326  genpcdl  7327  genpcuu  7328  genprndl  7329  genprndu  7330  distrlem1prl  7390  distrlem1pru  7391  ltsopr  7404  addcmpblnr  7547  ltsrprg  7555  addclsr  7561  mulclsr  7562  addasssrg  7564  addresr  7645  mulresr  7646  axaddass  7680  axmulass  7681  axdistr  7682  mulgt0  7839  mul4  7894  add4  7923  2addsub  7976  addsubeq4  7977  sub4  8007  muladd  8146  mulsub  8163  add20i  8254  mulge0i  8382  mulap0b  8416  divmuldivap  8472  ltmul12a  8618  zmulcl  9107  uz2mulcl  9402  qaddcl  9427  qmulcl  9429  qreccl  9434  rpaddcl  9465  ge0addcl  9764  ge0xaddcl  9766  expge1  10330  rexanuz  10760  amgm2  10890  iooinsup  11046  mulcn2  11081  dvds2ln  11526  opoe  11592  omoe  11593  opeo  11594  omeo  11595  lcmgcd  11759  lcmdvds  11760  tgcl  12233  innei  12332  txbas  12427  txss12  12435  txbasval  12436  blsscls2  12662  qtopbasss  12690  bj-indind  13130