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  5775  poxp  6236  tfrlem7  6321  brecop  6628  th3qlem1  6640  oviec  6644  pmss12g  6678  addcmpblnq  7369  mulcmpblnq  7370  mulpipqqs  7375  mulclnq  7378  mulcanenq  7387  distrnqg  7389  mulcmpblnq0  7446  mulcanenq0ec  7447  mulclnq0  7454  nqnq0a  7456  nqnq0m  7457  distrnq0  7461  genipv  7511  genpelvl  7514  genpelvu  7515  genpml  7519  genpmu  7520  genpcdl  7521  genpcuu  7522  genprndl  7523  genprndu  7524  distrlem1prl  7584  distrlem1pru  7585  ltsopr  7598  addcmpblnr  7741  ltsrprg  7749  addclsr  7755  mulclsr  7756  addasssrg  7758  addresr  7839  mulresr  7840  axaddass  7874  axmulass  7875  axdistr  7876  mulgt0  8035  mul4  8092  add4  8121  2addsub  8174  addsubeq4  8175  sub4  8205  muladd  8344  mulsub  8361  add20i  8452  mulge0i  8580  mulap0b  8615  divmuldivap  8672  ltmul12a  8820  zmulcl  9309  uz2mulcl  9611  qaddcl  9638  qmulcl  9640  qreccl  9645  rpaddcl  9680  ge0addcl  9984  ge0xaddcl  9986  expge1  10560  rexanuz  11000  amgm2  11130  iooinsup  11288  mulcn2  11323  dvds2ln  11834  opoe  11903  omoe  11904  opeo  11905  omeo  11906  lcmgcd  12081  lcmdvds  12082  pc2dvds  12332  tgcl  13752  innei  13851  txbas  13946  txss12  13954  txbasval  13955  blsscls2  14181  qtopbasss  14209  lgslem3  14591  bj-indind  14872