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  2137  eqtr2  2215  pm13.181  2449  rmob  3082  disjne  3504  seex  4370  tron  4417  fssres  5433  funbrfvb  5603  funopfvb  5604  fvelrnb  5608  fvco  5631  fvimacnvi  5676  ffvresb  5725  funresdfunsnss  5765  fvtp2g  5771  fvtp2  5774  fnex  5784  funex  5785  1st2nd  6239  dftpos4  6321  nnmsucr  6546  nnmcan  6577  xpmapenlem  6910  fundmfibi  7004  sup3exmid  8984  nzadd  9378  peano5uzti  9434  fnn0ind  9442  uztrn2  9619  irradd  9720  xltnegi  9910  xaddnemnf  9932  xaddnepnf  9933  xaddcom  9936  xnegdi  9943  elioore  9987  uzsubsubfz1  10123  fzo1fzo0n0  10259  elfzonelfzo  10306  qbtwnxr  10347  faclbnd  10833  faclbnd3  10835  dvdsprime  12290  pcgcd  12498  znf1o  14207  restuni  14408  stoig  14409  cnnei  14468  tgioo  14790  divcnap  14801  ivthdich  14889  lgsdi  15278  bj-indind  15578