Theorem an4s 588

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 586	. 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  589  anandis  592  anandirs  593  trin2  5061  fnun  5364  2elresin  5369  f1co  5475  f1oun  5524  f1oco  5527  f1mpt  5818  poxp  6290  tfrlem7  6375  brecop  6684  th3qlem1  6696  oviec  6700  pmss12g  6734  addcmpblnq  7434  mulcmpblnq  7435  mulpipqqs  7440  mulclnq  7443  mulcanenq  7452  distrnqg  7454  mulcmpblnq0  7511  mulcanenq0ec  7512  mulclnq0  7519  nqnq0a  7521  nqnq0m  7522  distrnq0  7526  genipv  7576  genpelvl  7579  genpelvu  7580  genpml  7584  genpmu  7585  genpcdl  7586  genpcuu  7587  genprndl  7588  genprndu  7589  distrlem1prl  7649  distrlem1pru  7650  ltsopr  7663  addcmpblnr  7806  ltsrprg  7814  addclsr  7820  mulclsr  7821  addasssrg  7823  addresr  7904  mulresr  7905  axaddass  7939  axmulass  7940  axdistr  7941  mulgt0  8101  mul4  8158  add4  8187  2addsub  8240  addsubeq4  8241  sub4  8271  muladd  8410  mulsub  8427  add20i  8519  mulge0i  8647  mulap0b  8682  divmuldivap  8739  ltmul12a  8887  zmulcl  9379  uz2mulcl  9682  qaddcl  9709  qmulcl  9711  qreccl  9716  rpaddcl  9752  ge0addcl  10056  ge0xaddcl  10058  expge1  10668  rexanuz  11153  amgm2  11283  iooinsup  11442  mulcn2  11477  dvds2ln  11989  opoe  12060  omoe  12061  opeo  12062  omeo  12063  lcmgcd  12246  lcmdvds  12247  pc2dvds  12499  tgcl  14300  innei  14399  txbas  14494  txss12  14502  txbasval  14503  blsscls2  14729  qtopbasss  14757  lgslem3  15243  bj-indind  15578