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  2106  eqtr2  2184  pm13.181  2418  rmob  3043  disjne  3462  seex  4313  tron  4360  fssres  5363  funbrfvb  5529  funopfvb  5530  fvelrnb  5534  fvco  5556  fvimacnvi  5599  ffvresb  5648  funresdfunsnss  5688  fvtp2g  5694  fvtp2  5697  fnex  5707  funex  5708  1st2nd  6149  dftpos4  6231  nnmsucr  6456  nnmcan  6487  xpmapenlem  6815  fundmfibi  6904  sup3exmid  8852  nzadd  9243  peano5uzti  9299  fnn0ind  9307  uztrn2  9483  irradd  9584  xltnegi  9771  xaddnemnf  9793  xaddnepnf  9794  xaddcom  9797  xnegdi  9804  elioore  9848  uzsubsubfz1  9983  fzo1fzo0n0  10118  elfzonelfzo  10165  qbtwnxr  10193  faclbnd  10654  faclbnd3  10656  dvdsprime  12054  pcgcd  12260  restuni  12812  stoig  12813  cnnei  12872  tgioo  13186  divcnap  13195  lgsdi  13578  bj-indind  13814