Theorem sylanb 284

Description: A syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
sylanb.1	|- ( ph <-> ps )
sylanb.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylanb	|- ( ( ph /\ ch ) -> th )

Proof of Theorem sylanb

Step	Hyp	Ref	Expression
1		sylanb.1	. . 3 |- ( ph <-> ps )
2	1	biimpi 120	. 2 |- ( ph -> ps )
3		sylanb.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan 283	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

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:  syl2anb  291  anabsan  577  2exeu  2175  eqtr2  2253  pm13.181  2496  rmob  3139  disjne  3566  seex  4461  tron  4508  fssres  5545  funbrfvb  5722  funopfvb  5723  fvelrnb  5729  fvco  5752  fvimacnvi  5797  ffvresb  5845  fcof  5868  funresdfunsnss  5892  fvtp2g  5898  fvtp2  5901  fnex  5911  funex  5914  1st2nd  6388  imacosuppfn  6481  dftpos4  6507  nnmsucr  6734  nnmcan  6765  xpmapenlem  7115  fundmfibi  7218  sup3exmid  9248  nzadd  9647  peano5uzti  9704  fnn0ind  9712  uztrn2  9890  irradd  9996  xltnegi  10187  xaddnemnf  10209  xaddnepnf  10210  xaddcom  10213  xnegdi  10220  elioore  10264  uzsubsubfz1  10402  fzo1fzo0n0  10544  elfzonelfzo  10597  qbtwnxr  10641  faclbnd  11128  faclbnd3  11130  swrdccat3b  11457  dvdsprime  12844  pcgcd  13052  znf1o  14925  restuni  15163  stoig  15164  cnnei  15223  tgioo  15545  divcnap  15556  ivthdich  15644  lgsdi  16036  bj-indind  16828