Theorem sylibrd 167

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylibrd.1	|- ( ph -> ( ps -> ch ) )
sylibrd.2	|- ( ph -> ( th <-> ch ) )

Assertion

Ref	Expression
sylibrd	|- ( ph -> ( ps -> th ) )

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		sylibrd.2	. . 3 |- ( ph -> ( th <-> ch ) )
3	2	biimprd 156	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	syld 44	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> 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:  3imtr4d  201  sbciegft  2844  opeldmg  4558  elreldm  4578  ssimaex  5255  f1eqcocnv  5451  fliftfun  5456  isopolem  5481  isosolem  5483  brtposg  5892  issmo2  5927  rdgon  5996  frecsuclem3  6013  freccl  6016  nnmcl  6083  nnawordi  6111  nnmordi  6112  nnmord  6113  swoord1  6158  ecopovtrn  6226  ecopovtrng  6229  f1domg  6261  supmoti  6406  isotilem  6419  enq0tr  6624  prubl  6676  ltexprlemloc  6797  addextpr  6811  recexprlem1ssl  6823  recexprlem1ssu  6824  cauappcvgprlemdisj  6841  mulcmpblnr  6918  mulgt0sr  6954  ltleletr  7193  ltle  7198  ltadd2  7523  leltadd  7551  reapti  7679  apreap  7687  reapcotr  7698  apcotr  7707  addext  7710  mulext1  7712  zapne  8422  zextle  8438  prime  8446  uzin  8651  indstr  8681  supinfneg  8683  infsupneg  8684  ublbneg  8698  xrltle  8873  xrre2  8888  icc0r  8949  fzrevral  9122  flqge  9284  modqadd1  9363  modqmul1  9379  facdiv  9665  resqrexlemgt0  9906  abs00ap  9948  absext  9949  climshftlemg  10141  climcaucn  10188  dvds2lem  10207  dvdsfac  10260  ltoddhalfle  10293  ndvdsadd  10331  gcdaddm  10375  bezoutlembi  10394  gcdzeq  10411  ialgcvga  10433  rpdvds  10481  cncongr1  10485  cncongr2  10486  prmind2  10502  euclemma  10525  isprm6  10526  rpexp  10532  sqrt2irr  10541