Theorem sylan2b 282

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	|- ( ph <-> ch )
sylan2b.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylan2b	|- ( ( ps /\ ph ) -> th )

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 |- ( ph <-> ch )
2	1	biimpi 119	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 281	1 |- ( ( ps /\ ph ) -> th )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  286  dcor  882  bm1.1  2074  eqtr3  2108  morex  2802  reuss2  3282  reupick  3286  rabsneu  3521  opabss  3910  triun  3957  poirr  4145  wepo  4197  wetrep  4198  rexxfrd  4300  reg3exmidlemwe  4409  nnsuc  4445  fnfco  5200  fun11iun  5289  fnressn  5499  fvpr1g  5519  fvtp1g  5521  fvtp3g  5523  fvtp3  5526  f1mpt  5566  caovlem2d  5853  offval  5879  dfoprab3  5977  1stconst  6002  2ndconst  6003  poxp  6013  tfrlemisucaccv  6106  tfr1onlemsucaccv  6122  tfrcllemsucaccv  6135  fiintim  6695  addclpi  6949  addnidpig  6958  reapmul1  8135  nnnn0addcl  8766  un0addcl  8769  un0mulcl  8770  zltnle  8859  nn0ge0div  8896  uzind3  8922  uzind4  9139  ltsubrp  9231  ltaddrp  9232  xrlttr  9328  xrltso  9329  xltnegi  9360  fzind2  9713  qltnle  9720  qbtwnxr  9732  exp3vallem  10019  expp1  10025  expnegap0  10026  expcllem  10029  mulexpzap  10058  expaddzap  10062  expmulzap  10064  hashunlem  10275  shftf  10327  sqrtdiv  10538  mulcn2  10764  isummolem2  10835  cvgratz  10989  dvdsflip  11193  dvdsfac  11202  lcmgcdlem  11400  rpexp1i  11474  hashdvds  11538  hashgcdlem  11544  bj-bdfindes  12148  bj-findes  12180