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  2118  eqtr2  2196  pm13.181  2429  rmob  3055  disjne  3476  seex  4334  tron  4381  fssres  5390  funbrfvb  5557  funopfvb  5558  fvelrnb  5562  fvco  5585  fvimacnvi  5629  ffvresb  5678  funresdfunsnss  5718  fvtp2g  5724  fvtp2  5727  fnex  5737  funex  5738  1st2nd  6179  dftpos4  6261  nnmsucr  6486  nnmcan  6517  xpmapenlem  6846  fundmfibi  6935  sup3exmid  8910  nzadd  9301  peano5uzti  9357  fnn0ind  9365  uztrn2  9541  irradd  9642  xltnegi  9831  xaddnemnf  9853  xaddnepnf  9854  xaddcom  9857  xnegdi  9864  elioore  9908  uzsubsubfz1  10043  fzo1fzo0n0  10178  elfzonelfzo  10225  qbtwnxr  10253  faclbnd  10714  faclbnd3  10716  dvdsprime  12114  pcgcd  12320  restuni  13543  stoig  13544  cnnei  13603  tgioo  13917  divcnap  13926  lgsdi  14309  bj-indind  14544