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  3505  seex  4371  tron  4418  fssres  5436  funbrfvb  5606  funopfvb  5607  fvelrnb  5611  fvco  5634  fvimacnvi  5679  ffvresb  5728  funresdfunsnss  5768  fvtp2g  5774  fvtp2  5777  fnex  5787  funex  5788  1st2nd  6248  dftpos4  6330  nnmsucr  6555  nnmcan  6586  xpmapenlem  6919  fundmfibi  7013  sup3exmid  9001  nzadd  9395  peano5uzti  9451  fnn0ind  9459  uztrn2  9636  irradd  9737  xltnegi  9927  xaddnemnf  9949  xaddnepnf  9950  xaddcom  9953  xnegdi  9960  elioore  10004  uzsubsubfz1  10140  fzo1fzo0n0  10276  elfzonelfzo  10323  qbtwnxr  10364  faclbnd  10850  faclbnd3  10852  dvdsprime  12315  pcgcd  12523  znf1o  14283  restuni  14492  stoig  14493  cnnei  14552  tgioo  14874  divcnap  14885  ivthdich  14973  lgsdi  15362  bj-indind  15662