Theorem an4s 555

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 553	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) )
2		an4s.1	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
3	1, 2	sylbi 119	1 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  an42s  556  anandis  559  anandirs  560  trin2  4823  fnun  5120  2elresin  5125  f1co  5228  f1oun  5273  f1oco  5276  f1mpt  5550  poxp  5997  tfrlem7  6082  brecop  6380  th3qlem1  6392  oviec  6396  pmss12g  6430  addcmpblnq  6924  mulcmpblnq  6925  mulpipqqs  6930  mulclnq  6933  mulcanenq  6942  distrnqg  6944  mulcmpblnq0  7001  mulcanenq0ec  7002  mulclnq0  7009  nqnq0a  7011  nqnq0m  7012  distrnq0  7016  genipv  7066  genpelvl  7069  genpelvu  7070  genpml  7074  genpmu  7075  genpcdl  7076  genpcuu  7077  genprndl  7078  genprndu  7079  distrlem1prl  7139  distrlem1pru  7140  ltsopr  7153  addcmpblnr  7283  ltsrprg  7291  addclsr  7297  mulclsr  7298  addasssrg  7300  addresr  7372  mulresr  7373  axaddass  7405  axmulass  7406  axdistr  7407  mulgt0  7558  mul4  7612  add4  7641  2addsub  7694  addsubeq4  7695  sub4  7725  muladd  7860  mulsub  7877  add20i  7968  mulge0i  8095  mulap0b  8122  divmuldivap  8177  ltmul12a  8319  zmulcl  8801  uz2mulcl  9093  qaddcl  9118  qmulcl  9120  qreccl  9125  rpaddcl  9155  ge0addcl  9397  expge1  9988  rexanuz  10417  amgm2  10547  mulcn2  10697  dvds2ln  11103  opoe  11169  omoe  11170  opeo  11171  omeo  11172  lcmgcd  11334  lcmdvds  11335  bj-indind  11782