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  581  2exeu  2179  eqtr2  2257  pm13.181  2502  rmob  3145  disjne  3577  seex  4475  tron  4522  fssres  5560  funbrfvb  5737  funopfvb  5738  fvelrnb  5744  fvco  5769  fvimacnvi  5814  ffvresb  5862  fcof  5885  funresdfunsnss  5909  fvtp2g  5915  fvtp2  5918  fnex  5928  funex  5931  1st2nd  6405  imacosuppfn  6498  dftpos4  6524  nnmsucr  6751  nnmcan  6782  xpmapenlem  7139  fundmfibi  7242  sup3exmid  9277  nzadd  9676  peano5uzti  9733  fnn0ind  9741  uztrn2  9919  irradd  10025  xltnegi  10216  xaddnemnf  10238  xaddnepnf  10239  xaddcom  10242  xnegdi  10249  elioore  10293  uzsubsubfz1  10431  fzo1fzo0n0  10573  elfzonelfzo  10626  qbtwnxr  10670  faclbnd  11157  faclbnd3  11159  swrdccat3b  11490  dvdsprime  12878  pcgcd  13086  znf1o  14958  restuni  15196  stoig  15197  cnnei  15256  tgioo  15578  divcnap  15589  ivthdich  15677  lgsdi  16070  bj-indind  16872