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 527  3imtr3d 541  euim 1419  sbcbid 1972  sbc19.20dv 1981  ra4esbca 1995  csbeq2d 2014  ra4csbela 2038  reuuniss2 2886  ordzsl 3111  fvopab2 3782  oaword2 4177  oaordex 4182  omword1 4194  om00 4196  oen0 4203  oeordi 4204  php3 4501  onomeneq 4504  fodomfib 4547  suc11reg 4585  rankr1 4654  aceq3lem 4712  ac6lem 4734  cardne 4810  cardaleph 4865  ltexpq 5060  addclprlem1 5098  addclprlem2 5099  mulclprlem 5101  ltexprlem7 5128  prlem936b 5134  reclem4pr 5139  sqgt0sr 5195  cnegextlem1 5325  addcan 5331  mulcan 5667  mulgt1t 5809  nnleltp1t 5909  lt2halvest 5997  zextltt 6145  recnzt 6146  zeot 6154  uzindOLD 6164  flwordit 6191  qbtwnre 6224  sqr2irr 6667  facndivt 6888  fsum1s 6955  2climnn 7047  2climnn0 7048  climge0 7057  climaddlem3 7060  caucvglem5 7105  caucvglem6 7106  caucvg 7107  serzf0 7113  ser1f0 7114  cvgratlem1ALT 7190  cvgratlem1 7193  cvgratlem2 7194  dnsconst 7738  lmnn 7887  lmuni 7902  lmle 7911  metelcls 7916  metcnp4 7920  cmsss 7947  blocnilem 8408  ip2eqi 8461  minveclem27 8515  minveceu 8527  sincosq3sgn 8642  sincosq4sgn 8643  eff1i 8683  hial0 8907  hial02 8908  hial2eqt 8911  chocuni 9111  shlej1t 9293  h1datom 9444  sumspansnt 9534  lnopcnbdt 9903  riesz4 9934  bra11 9979  pjss2co 10030  pjnormss 10034  pjorthco 10035  pjclem4a 10064  pj3lem1 10072  pj3cor1 10075  hst1ht 10092  stm1 10108  strlem1 10115  golem2 10137  mdbr2 10161  mdsl2 10186  atexcht 10245  atcvatlem 10249  irredlem1 10254  cdjreu 10293  cdj1 10294  cdj3lem1 10295  ghomf1olem 10330  idmon 10624

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