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  2170  eqtr2  2248  pm13.181  2482  rmob  3122  disjne  3545  seex  4426  tron  4473  fssres  5501  funbrfvb  5674  funopfvb  5675  fvelrnb  5681  fvco  5704  fvimacnvi  5749  ffvresb  5798  funresdfunsnss  5842  fvtp2g  5848  fvtp2  5851  fnex  5861  funex  5862  1st2nd  6327  dftpos4  6409  nnmsucr  6634  nnmcan  6665  xpmapenlem  7010  fundmfibi  7105  sup3exmid  9104  nzadd  9499  peano5uzti  9555  fnn0ind  9563  uztrn2  9740  irradd  9841  xltnegi  10031  xaddnemnf  10053  xaddnepnf  10054  xaddcom  10057  xnegdi  10064  elioore  10108  uzsubsubfz1  10244  fzo1fzo0n0  10383  elfzonelfzo  10436  qbtwnxr  10477  faclbnd  10963  faclbnd3  10965  swrdccat3b  11272  dvdsprime  12644  pcgcd  12852  znf1o  14615  restuni  14846  stoig  14847  cnnei  14906  tgioo  15228  divcnap  15239  ivthdich  15327  lgsdi  15716  bj-indind  16295