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  575  2exeu  2146  eqtr2  2224  pm13.181  2458  rmob  3091  disjne  3514  seex  4382  tron  4429  fssres  5451  funbrfvb  5621  funopfvb  5622  fvelrnb  5626  fvco  5649  fvimacnvi  5694  ffvresb  5743  funresdfunsnss  5787  fvtp2g  5793  fvtp2  5796  fnex  5806  funex  5807  1st2nd  6267  dftpos4  6349  nnmsucr  6574  nnmcan  6605  xpmapenlem  6946  fundmfibi  7040  sup3exmid  9030  nzadd  9425  peano5uzti  9481  fnn0ind  9489  uztrn2  9666  irradd  9767  xltnegi  9957  xaddnemnf  9979  xaddnepnf  9980  xaddcom  9983  xnegdi  9990  elioore  10034  uzsubsubfz1  10170  fzo1fzo0n0  10307  elfzonelfzo  10359  qbtwnxr  10400  faclbnd  10886  faclbnd3  10888  dvdsprime  12444  pcgcd  12652  znf1o  14413  restuni  14644  stoig  14645  cnnei  14704  tgioo  15026  divcnap  15037  ivthdich  15125  lgsdi  15514  bj-indind  15868