Theorem sylbird 222

Description: A syllogism deduction.

Hypotheses

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

Assertion

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

Proof of Theorem sylbird

Step	Hyp	Ref	Expression
1		sylbird.1	. . 3 |- (ph -> (ch <-> ps))
2	1	biimprd 171	. 2 |- (ph -> (ps -> ch))
3		sylbird.2	. 2 |- (ph -> (ch -> th))
4	2, 3	syld 30	1 |- (ph -> (ps -> th))

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

This theorem is referenced by:  3imtr3d 601  hbsbc1g 2461  ordsssuc2OLD 3759  tfindsg 3944  tfindsg2 3945  limom 3967  nnsuc 3969  findsg 3980  tfrlem9 5127  oe0lem 5197  oa00 5241  omwordi 5250  om00 5254  omass 5259  oelim2 5270  oeoa 5272  oeoe 5274  dom2d 5463  ac6sfilem3 5508  rankr1lem 5784  unidom 5970  alephnbtwn 6016  alephval2 6050  axpowndlem3 6103  distrlem4pr 6282  sqgt0sr 6367  suppsr3 6376  renegcli 6576  renegcliOLD 6577  xrletri 6736  letric 6802  letricOLD 6803  redivcli 6976  nnge1 7126  nnleltp1 7138  nnsubi 7140  avgle 7231  uzind2 7418  uzwo4OLD 7422  nn0ind-raph 7426  zbtwnre 7434  qsqueeze 7461  monoord 7523  icounlem 7581  uzwo 7624  uzwoOLD 7625  om2uzf1oi 7712  cvg2i 8174  facdiv 8194  facwordi 8196  caucvgi 8423  infcvglem3 8484  znnenlem 8770  infpnlem1 8775  infxpidmlem5 8825  infxpidmlem11 8831  qdensere 9027  metxp 9111  metcnp 9165  cmsss 9275  bcthlem18 9294  bcthlem28 9304  minveclem25 9914  spwval2 9996  efifolem5 10080  efif1lem4 10087  oprabvaligg 10154  ficard 10176  cdrci 10182  flimopn 10321  dvrunz 10419  hlimcauii 10739  occllem6 10811  shmodsi 10995  nmcopexlem6 11593  nmcfnexlem6 11622  rnbra 11678  bra11 11679  atcvati 11958  atcvat2i 11959  irredlem4 11965  atmd2 11972  sumdmdlem 11990  addltmulALT 12018  fzind 13610  fnn0ind 13611  dvdsleabs 13694  algcvgblem 13745  eucalgcvga 13754  soseq 13955  mappow 14413  iintlem1 15010  subtr 15352  subtr2 15353  ufilss 15567  fsumlt1 15831  ismtyres 15954  heiborlem35 15989  rrntotbnd 16022  iccbnd 16026  grpkerinj 16042  pcopt 16084  pcoass 16085  pcorevlem 16086  isringd 16097  iscringd 16147  isdmn3 16222  dmncan1 16224  erreft2 16261  ordintdif 16440  atomnle 17016  hlexch3 17041  hlexch4 17042  hlatexchb1 17043  cvrat2 17066  ps-1 17078  ps2 17079

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 164

Copyright terms: Public domain