Theorem an4s 552

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 550	. 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  553  anandis  556  anandirs  557  trin2  4736  fnun  5025  2elresin  5030  f1co  5121  f1oun  5166  f1oco  5169  f1mpt  5431  poxp  5873  tfrlem7  5956  brecop  6219  th3qlem1  6231  oviec  6235  addcmpblnq  6557  mulcmpblnq  6558  mulpipqqs  6563  mulclnq  6566  mulcanenq  6575  distrnqg  6577  mulcmpblnq0  6634  mulcanenq0ec  6635  mulclnq0  6642  nqnq0a  6644  nqnq0m  6645  distrnq0  6649  genipv  6699  genpelvl  6702  genpelvu  6703  genpml  6707  genpmu  6708  genpcdl  6709  genpcuu  6710  genprndl  6711  genprndu  6712  distrlem1prl  6772  distrlem1pru  6773  ltsopr  6786  addcmpblnr  6916  ltsrprg  6924  addclsr  6930  mulclsr  6931  addasssrg  6933  addresr  7005  mulresr  7006  axaddass  7038  axmulass  7039  axdistr  7040  mulgt0  7186  mul4  7240  add4  7269  2addsub  7322  addsubeq4  7323  sub4  7353  muladd  7488  mulsub  7505  add20i  7593  mulge0i  7720  mulap0b  7745  divmuldivap  7800  ltmul12a  7938  zmulcl  8404  uz2mulcl  8695  qaddcl  8720  qmulcl  8722  qreccl  8727  rpaddcl  8757  ge0addcl  9004  serige0  9473  expge1  9513  rexanuz  9874  amgm2  10004  mulcn2  10151  dvds2ln  10228  opoe  10295  omoe  10296  opeo  10297  omeo  10298  lcmgcd  10460  lcmdvds  10461  bj-indind  10727