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  2134  eqtr2  2212  pm13.181  2446  rmob  3078  disjne  3500  seex  4366  tron  4413  fssres  5429  funbrfvb  5599  funopfvb  5600  fvelrnb  5604  fvco  5627  fvimacnvi  5672  ffvresb  5721  funresdfunsnss  5761  fvtp2g  5767  fvtp2  5770  fnex  5780  funex  5781  1st2nd  6234  dftpos4  6316  nnmsucr  6541  nnmcan  6572  xpmapenlem  6905  fundmfibi  6997  sup3exmid  8976  nzadd  9369  peano5uzti  9425  fnn0ind  9433  uztrn2  9610  irradd  9711  xltnegi  9901  xaddnemnf  9923  xaddnepnf  9924  xaddcom  9927  xnegdi  9934  elioore  9978  uzsubsubfz1  10114  fzo1fzo0n0  10250  elfzonelfzo  10297  qbtwnxr  10326  faclbnd  10812  faclbnd3  10814  dvdsprime  12260  pcgcd  12467  znf1o  14139  restuni  14340  stoig  14341  cnnei  14400  tgioo  14714  divcnap  14723  ivthdich  14807  lgsdi  15153  bj-indind  15424