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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl2anb  291  anabsan  581  2exeu  2179  eqtr2  2257  pm13.181  2502  rmob  3145  disjne  3578  seex  4480  tron  4527  fssres  5565  funbrfvb  5743  funopfvb  5744  fvelrnb  5750  fvco  5775  fvimacnvi  5823  ffvresb  5871  fcof  5894  funresdfunsnss  5918  fvtp2g  5924  fvtp2  5927  fnex  5937  funex  5940  1st2nd  6415  imacosuppfn  6508  dftpos4  6534  nnmsucr  6761  nnmcan  6792  xpmapenlem  7149  fundmfibi  7252  sup3exmid  9287  nzadd  9697  peano5uzti  9754  fnn0ind  9762  uztrn2  9940  irradd  10046  xltnegi  10237  xaddnemnf  10259  xaddnepnf  10260  xaddcom  10263  xnegdi  10270  elioore  10314  uzsubsubfz1  10453  fzo1fzo0n0  10595  elfzonelfzo  10648  qbtwnxr  10692  faclbnd  11179  faclbnd3  11181  swrdccat3b  11512  dvdsprime  12900  pcgcd  13108  znf1o  14986  restuni  15273  stoig  15274  cnnei  15333  tgioo  15655  divcnap  15666  ivthdich  15754  lgsdi  16156  bj-indind  16958