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  4482  tron  4529  fssres  5568  funbrfvb  5746  funopfvb  5747  fvelrnb  5753  fvco  5778  fvimacnvi  5826  ffvresb  5874  fcof  5897  funresdfunsnss  5921  fvtp2g  5927  fvtp2  5930  fnex  5940  funex  5943  1st2nd  6419  imacosuppfn  6512  dftpos4  6538  nnmsucr  6765  nnmcan  6796  xpmapenlem  7153  fundmfibi  7256  sup3exmid  9295  nzadd  9708  peano5uzti  9765  fnn0ind  9773  uztrn2  9956  irradd  10062  xltnegi  10254  xaddnemnf  10276  xaddnepnf  10277  xaddcom  10280  xnegdi  10287  elioore  10331  uzsubsubfz1  10470  fzo1fzo0n0  10612  elfzonelfzo  10665  qbtwnxr  10709  faclbnd  11201  faclbnd3  11203  swrdccat3b  11534  dvdsprime  12925  pcgcd  13137  cntri  14165  cntzsgrpcl  14167  znf1o  15095  restuni  15398  stoig  15399  cnnei  15458  tgioo  15780  divcnap  15791  ivthdich  15879  lgsdi  16361  bj-indind  17163