Theorem sylanb 280

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 279	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  287  anabsan  545  2exeu  2052  eqtr2  2118  pm13.181  2349  rmob  2953  disjne  3363  seex  4195  tron  4242  fssres  5234  funbrfvb  5396  funopfvb  5397  fvelrnb  5401  fvco  5423  fvimacnvi  5466  ffvresb  5515  funresdfunsnss  5555  fvtp2g  5561  fvtp2  5564  fnex  5574  funex  5575  1st2nd  6009  dftpos4  6090  nnmsucr  6314  nnmcan  6345  xpmapenlem  6672  fundmfibi  6755  sup3exmid  8573  nzadd  8958  peano5uzti  9011  fnn0ind  9019  uztrn2  9193  irradd  9288  xltnegi  9459  xaddnemnf  9481  xaddnepnf  9482  xaddcom  9485  xnegdi  9492  elioore  9536  uzsubsubfz1  9669  fzo1fzo0n0  9801  elfzonelfzo  9848  qbtwnxr  9876  faclbnd  10328  faclbnd3  10330  dvdsprime  11596  restuni  12123  stoig  12124  cnnei  12182  tgioo  12465  bj-indind  12715