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  3057  disjne  3478  seex  4337  tron  4384  fssres  5393  funbrfvb  5560  funopfvb  5561  fvelrnb  5565  fvco  5588  fvimacnvi  5632  ffvresb  5681  funresdfunsnss  5721  fvtp2g  5727  fvtp2  5730  fnex  5740  funex  5741  1st2nd  6184  dftpos4  6266  nnmsucr  6491  nnmcan  6522  xpmapenlem  6851  fundmfibi  6940  sup3exmid  8916  nzadd  9307  peano5uzti  9363  fnn0ind  9371  uztrn2  9547  irradd  9648  xltnegi  9837  xaddnemnf  9859  xaddnepnf  9860  xaddcom  9863  xnegdi  9870  elioore  9914  uzsubsubfz1  10050  fzo1fzo0n0  10185  elfzonelfzo  10232  qbtwnxr  10260  faclbnd  10723  faclbnd3  10725  dvdsprime  12124  pcgcd  12330  restuni  13711  stoig  13712  cnnei  13771  tgioo  14085  divcnap  14094  lgsdi  14477  bj-indind  14723