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  2146  eqtr2  2224  pm13.181  2458  rmob  3091  disjne  3514  seex  4383  tron  4430  fssres  5453  funbrfvb  5623  funopfvb  5624  fvelrnb  5628  fvco  5651  fvimacnvi  5696  ffvresb  5745  funresdfunsnss  5789  fvtp2g  5795  fvtp2  5798  fnex  5808  funex  5809  1st2nd  6269  dftpos4  6351  nnmsucr  6576  nnmcan  6607  xpmapenlem  6948  fundmfibi  7042  sup3exmid  9032  nzadd  9427  peano5uzti  9483  fnn0ind  9491  uztrn2  9668  irradd  9769  xltnegi  9959  xaddnemnf  9981  xaddnepnf  9982  xaddcom  9985  xnegdi  9992  elioore  10036  uzsubsubfz1  10172  fzo1fzo0n0  10309  elfzonelfzo  10361  qbtwnxr  10402  faclbnd  10888  faclbnd3  10890  dvdsprime  12477  pcgcd  12685  znf1o  14446  restuni  14677  stoig  14678  cnnei  14737  tgioo  15059  divcnap  15070  ivthdich  15158  lgsdi  15547  bj-indind  15905