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  571  2exeu  2112  eqtr2  2190  pm13.181  2423  rmob  3048  disjne  3469  seex  4321  tron  4368  fssres  5375  funbrfvb  5542  funopfvb  5543  fvelrnb  5547  fvco  5570  fvimacnvi  5614  ffvresb  5663  funresdfunsnss  5703  fvtp2g  5709  fvtp2  5712  fnex  5722  funex  5723  1st2nd  6164  dftpos4  6246  nnmsucr  6471  nnmcan  6502  xpmapenlem  6831  fundmfibi  6920  sup3exmid  8877  nzadd  9268  peano5uzti  9324  fnn0ind  9332  uztrn2  9508  irradd  9609  xltnegi  9796  xaddnemnf  9818  xaddnepnf  9819  xaddcom  9822  xnegdi  9829  elioore  9873  uzsubsubfz1  10008  fzo1fzo0n0  10143  elfzonelfzo  10190  qbtwnxr  10218  faclbnd  10679  faclbnd3  10681  dvdsprime  12080  pcgcd  12286  restuni  13051  stoig  13052  cnnei  13111  tgioo  13425  divcnap  13434  lgsdi  13817  bj-indind  14052