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  3079  disjne  3501  seex  4367  tron  4414  fssres  5430  funbrfvb  5600  funopfvb  5601  fvelrnb  5605  fvco  5628  fvimacnvi  5673  ffvresb  5722  funresdfunsnss  5762  fvtp2g  5768  fvtp2  5771  fnex  5781  funex  5782  1st2nd  6236  dftpos4  6318  nnmsucr  6543  nnmcan  6574  xpmapenlem  6907  fundmfibi  6999  sup3exmid  8978  nzadd  9372  peano5uzti  9428  fnn0ind  9436  uztrn2  9613  irradd  9714  xltnegi  9904  xaddnemnf  9926  xaddnepnf  9927  xaddcom  9930  xnegdi  9937  elioore  9981  uzsubsubfz1  10117  fzo1fzo0n0  10253  elfzonelfzo  10300  qbtwnxr  10329  faclbnd  10815  faclbnd3  10817  dvdsprime  12263  pcgcd  12470  znf1o  14150  restuni  14351  stoig  14352  cnnei  14411  tgioo  14733  divcnap  14744  ivthdich  14832  lgsdi  15194  bj-indind  15494