Theorem sylibrd 168

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 157	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	syld 45	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4d  202  sbciegft  2985  opeldmg  4816  elreldm  4837  ssimaex  5557  resflem  5660  f1eqcocnv  5770  fliftfun  5775  isopolem  5801  isosolem  5803  brtposg  6233  issmo2  6268  nnmcl  6460  nnawordi  6494  nnmordi  6495  nnmord  6496  swoord1  6542  ecopovtrn  6610  ecopovtrng  6613  f1domg  6736  mapen  6824  mapxpen  6826  supmoti  6970  isotilem  6983  exmidomniim  7117  enq0tr  7396  prubl  7448  ltexprlemloc  7569  addextpr  7583  recexprlem1ssl  7595  recexprlem1ssu  7596  cauappcvgprlemdisj  7613  mulcmpblnr  7703  mulgt0sr  7740  map2psrprg  7767  ltleletr  8001  ltle  8007  ltadd2  8338  leltadd  8366  reapti  8498  apreap  8506  reapcotr  8517  apcotr  8526  addext  8529  mulext1  8531  zapne  9286  zextle  9303  prime  9311  uzin  9519  indstr  9552  supinfneg  9554  infsupneg  9555  ublbneg  9572  xrltle  9755  xrre2  9778  icc0r  9883  fzrevral  10061  flqge  10238  modqadd1  10317  modqmul1  10333  facdiv  10672  resqrexlemgt0  10984  abs00ap  11026  absext  11027  climshftlemg  11265  climcaucn  11314  dvds2lem  11765  dvdsfac  11820  ltoddhalfle  11852  ndvdsadd  11890  gcdaddm  11939  bezoutlembi  11960  gcdzeq  11977  algcvga  12005  rpdvds  12053  cncongr1  12057  cncongr2  12058  prmind2  12074  euclemma  12100  isprm6  12101  rpexp  12107  sqrt2irr  12116  odzdvds  12199  pclemub  12241  pceulem  12248  pc2dvds  12283  fldivp1  12300  infpnlem1  12311  prmunb  12314  fiinbas  12841  bastg  12855  tgcl  12858  opnssneib  12950  tgcnp  13003  iscnp4  13012  cnntr  13019  cnptopresti  13032  lmss  13040  lmtopcnp  13044  txdis  13071  xblss2ps  13198  xblss2  13199  blsscls2  13287  metequiv2  13290  bdxmet  13295  mulc1cncf  13370  cncfco  13372  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  lgsdir  13730  2sqlem8a  13752  2sqlem10  13755  triap  14061