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  9290  nzadd  9702  peano5uzti  9759  fnn0ind  9767  uztrn2  9950  irradd  10056  xltnegi  10248  xaddnemnf  10270  xaddnepnf  10271  xaddcom  10274  xnegdi  10281  elioore  10325  uzsubsubfz1  10464  fzo1fzo0n0  10606  elfzonelfzo  10659  qbtwnxr  10703  faclbnd  11195  faclbnd3  11197  swrdccat3b  11528  dvdsprime  12919  pcgcd  13131  cntri  14159  cntzsgrpcl  14161  znf1o  15070  restuni  15364  stoig  15365  cnnei  15424  tgioo  15746  divcnap  15757  ivthdich  15845  lgsdi  16322  bj-indind  17124