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  2148  eqtr2  2226  pm13.181  2460  rmob  3099  disjne  3522  seex  4400  tron  4447  fssres  5473  funbrfvb  5644  funopfvb  5645  fvelrnb  5649  fvco  5672  fvimacnvi  5717  ffvresb  5766  funresdfunsnss  5810  fvtp2g  5816  fvtp2  5819  fnex  5829  funex  5830  1st2nd  6290  dftpos4  6372  nnmsucr  6597  nnmcan  6628  xpmapenlem  6971  fundmfibi  7066  sup3exmid  9065  nzadd  9460  peano5uzti  9516  fnn0ind  9524  uztrn2  9701  irradd  9802  xltnegi  9992  xaddnemnf  10014  xaddnepnf  10015  xaddcom  10018  xnegdi  10025  elioore  10069  uzsubsubfz1  10205  fzo1fzo0n0  10344  elfzonelfzo  10396  qbtwnxr  10437  faclbnd  10923  faclbnd3  10925  swrdccat3b  11231  dvdsprime  12559  pcgcd  12767  znf1o  14528  restuni  14759  stoig  14760  cnnei  14819  tgioo  15141  divcnap  15152  ivthdich  15240  lgsdi  15629  bj-indind  16067