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  5022  fnun  5324  2elresin  5329  f1co  5435  f1oun  5483  f1oco  5486  f1mpt  5774  poxp  6235  tfrlem7  6320  brecop  6627  th3qlem1  6639  oviec  6643  pmss12g  6677  addcmpblnq  7368  mulcmpblnq  7369  mulpipqqs  7374  mulclnq  7377  mulcanenq  7386  distrnqg  7388  mulcmpblnq0  7445  mulcanenq0ec  7446  mulclnq0  7453  nqnq0a  7455  nqnq0m  7456  distrnq0  7460  genipv  7510  genpelvl  7513  genpelvu  7514  genpml  7518  genpmu  7519  genpcdl  7520  genpcuu  7521  genprndl  7522  genprndu  7523  distrlem1prl  7583  distrlem1pru  7584  ltsopr  7597  addcmpblnr  7740  ltsrprg  7748  addclsr  7754  mulclsr  7755  addasssrg  7757  addresr  7838  mulresr  7839  axaddass  7873  axmulass  7874  axdistr  7875  mulgt0  8034  mul4  8091  add4  8120  2addsub  8173  addsubeq4  8174  sub4  8204  muladd  8343  mulsub  8360  add20i  8451  mulge0i  8579  mulap0b  8614  divmuldivap  8671  ltmul12a  8819  zmulcl  9308  uz2mulcl  9610  qaddcl  9637  qmulcl  9639  qreccl  9644  rpaddcl  9679  ge0addcl  9983  ge0xaddcl  9985  expge1  10559  rexanuz  10999  amgm2  11129  iooinsup  11287  mulcn2  11322  dvds2ln  11833  opoe  11902  omoe  11903  opeo  11904  omeo  11905  lcmgcd  12080  lcmdvds  12081  pc2dvds  12331  tgcl  13603  innei  13702  txbas  13797  txss12  13805  txbasval  13806  blsscls2  14032  qtopbasss  14060  lgslem3  14442  bj-indind  14723