Theorem sylanb 278

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 118	. 2 |- ( ph -> ps )
3		sylanb.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan 277	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl2anb  285  anabsan  540  2exeu  2034  eqtr2  2100  pm13.181  2328  rmob  2907  disjne  3304  seex  4098  tron  4145  fssres  5097  funbrfvb  5248  funopfvb  5249  fvelrnb  5253  fvco  5275  fvimacnvi  5313  ffvresb  5360  fvtp2g  5402  fvtp2  5405  fnex  5415  funex  5416  1st2nd  5838  dftpos4  5912  nnmsucr  6132  nnmcan  6158  fundmfibi  6448  nzadd  8484  peano5uzti  8536  fnn0ind  8544  uztrn2  8717  irradd  8812  xltnegi  8978  elioore  9011  uzsubsubfz1  9143  fzo1fzo0n0  9269  elfzonelfzo  9316  qbtwnxr  9344  faclbnd  9765  faclbnd3  9767  dvdsprime  10648  bj-indind  10885