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  577  2exeu  2172  eqtr2  2250  pm13.181  2485  rmob  3126  disjne  3550  seex  4438  tron  4485  fssres  5520  funbrfvb  5695  funopfvb  5696  fvelrnb  5702  fvco  5725  fvimacnvi  5770  ffvresb  5818  fcof  5841  funresdfunsnss  5865  fvtp2g  5871  fvtp2  5874  fnex  5884  funex  5887  1st2nd  6353  imacosuppfn  6446  dftpos4  6472  nnmsucr  6699  nnmcan  6730  xpmapenlem  7078  fundmfibi  7180  sup3exmid  9196  nzadd  9593  peano5uzti  9649  fnn0ind  9657  uztrn2  9835  irradd  9941  xltnegi  10131  xaddnemnf  10153  xaddnepnf  10154  xaddcom  10157  xnegdi  10164  elioore  10208  uzsubsubfz1  10345  fzo1fzo0n0  10485  elfzonelfzo  10538  qbtwnxr  10580  faclbnd  11066  faclbnd3  11068  swrdccat3b  11387  dvdsprime  12774  pcgcd  12982  znf1o  14747  restuni  14983  stoig  14984  cnnei  15043  tgioo  15365  divcnap  15376  ivthdich  15464  lgsdi  15856  bj-indind  16648