Theorem sylibd 202

Description: A syllogism deduction.

Hypotheses

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

Assertion

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

Proof of Theorem sylibd

Step	Hyp	Ref	Expression
1		sylibd.1	. 2 |- (ph -> (ps -> ch))
2		sylibd.2	. . 3 |- (ph -> (ch <-> th))
3	2	biimpd 153	. 2 |- (ph -> (ch -> th))
4	1, 3	syld 27	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  bitrd 528  3imtr3d 542  euim 1421  sbcbid 1976  sbc19.20dv 1985  ra4esbca 1999  csbeq2d 2018  ra4csbela 2042  reuuniss2 2891  ordzsl 3116  fvopab2 3791  oaword2 4187  oaordex 4192  omword1 4204  om00 4206  oen0 4213  oeordi 4214  php3 4515  php3OLD 4516  onomeneq 4519  fodomfibOLD 4567  suc11reg 4605  rankr1 4674  aceq3lem 4732  ac6lem 4754  cardne 4830  cardaleph 4885  ltexpq 5080  addclprlem1 5118  addclprlem2 5119  mulclprlem 5121  ltexprlem7 5148  prlem936b 5154  reclem4pr 5159  sqgt0sr 5215  cnegextlem1 5345  addcan 5351  mulcan 5686  mulcanOLD 5687  mulgt1t 5845  nnleltp1t 5954  lt2halvest 6042  zextltt 6190  recnzt 6191  zeot 6199  uzindOLD 6208  flwordit 6237  qbtwnre 6278  sqr2irr 6729  facndivt 6943  fsum1s 7009  2climnn 7102  2climnn0 7103  climge0 7112  climaddlem3 7116  caucvglem5 7161  caucvglem6 7162  caucvg 7163  serzf0 7169  ser1f0 7170  cvgratlem1ALT 7247  cvgratlem1 7250  cvgratlem2 7251  dnsconst 7788  lmnn 7935  lmuni 7951  lmle 7960  metelcls 7965  metcnp4 7970  cmsss 7997  blocnilem 8464  ip2eqi 8517  minveclem27 8571  minveceu 8583  sincosq3sgn 8706  sincosq4sgn 8707  eff1i 8744  hial0 8968  hial02 8969  hial2eqt 8972  chocuni 9172  shlej1t 9355  h1datom 9504  sumspansnt 9594  lnopcnbdt 9965  riesz4 9996  bra11 10041  pjss2co 10092  pjnormss 10096  pjorthco 10097  pjclem4a 10126  pj3lem1 10134  pj3cor1 10137  hst1ht 10154  stm1 10170  strlem1 10177  golem2 10199  mdbr2 10223  dmdbr5 10235  mdsl2 10249  atexcht 10308  atcvatlem 10312  irredlem1 10317  cdjreu 10359  cdj1 10360  cdj3lem1 10361  ghomf1olem 10396  idmon 10745

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain