Theorem sylanb 282

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 119	. 2 |- ( ph -> ps )
3		sylanb.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan 281	1 |- ( ( ph /\ ch ) -> th )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  289  anabsan  565  2exeu  2105  eqtr2  2183  pm13.181  2416  rmob  3038  disjne  3457  seex  4307  tron  4354  fssres  5357  funbrfvb  5523  funopfvb  5524  fvelrnb  5528  fvco  5550  fvimacnvi  5593  ffvresb  5642  funresdfunsnss  5682  fvtp2g  5688  fvtp2  5691  fnex  5701  funex  5702  1st2nd  6141  dftpos4  6222  nnmsucr  6447  nnmcan  6478  xpmapenlem  6806  fundmfibi  6895  sup3exmid  8843  nzadd  9234  peano5uzti  9290  fnn0ind  9298  uztrn2  9474  irradd  9575  xltnegi  9762  xaddnemnf  9784  xaddnepnf  9785  xaddcom  9788  xnegdi  9795  elioore  9839  uzsubsubfz1  9973  fzo1fzo0n0  10108  elfzonelfzo  10155  qbtwnxr  10183  faclbnd  10643  faclbnd3  10645  dvdsprime  12033  pcgcd  12237  restuni  12713  stoig  12714  cnnei  12773  tgioo  13087  divcnap  13096  bj-indind  13649