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  564  2exeu  2091  eqtr2  2158  pm13.181  2390  rmob  3001  disjne  3416  seex  4257  tron  4304  fssres  5298  funbrfvb  5464  funopfvb  5465  fvelrnb  5469  fvco  5491  fvimacnvi  5534  ffvresb  5583  funresdfunsnss  5623  fvtp2g  5629  fvtp2  5632  fnex  5642  funex  5643  1st2nd  6079  dftpos4  6160  nnmsucr  6384  nnmcan  6415  xpmapenlem  6743  fundmfibi  6827  sup3exmid  8715  nzadd  9106  peano5uzti  9159  fnn0ind  9167  uztrn2  9343  irradd  9438  xltnegi  9618  xaddnemnf  9640  xaddnepnf  9641  xaddcom  9644  xnegdi  9651  elioore  9695  uzsubsubfz1  9828  fzo1fzo0n0  9960  elfzonelfzo  10007  qbtwnxr  10035  faclbnd  10487  faclbnd3  10489  dvdsprime  11803  restuni  12341  stoig  12342  cnnei  12401  tgioo  12715  divcnap  12724  bj-indind  13130