Theorem sylbird 205

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

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

This theorem is referenced by:  3imtr3d 542  hbsbc1g 1948  ordsssuc2 3059  limom 3146  nnsuc 3148  findsg 3157  tfindsg 3162  tfindsg2 3163  tfrlem9 3919  oe0lem 4152  oa00 4193  omwordi 4202  om00 4206  omass 4211  oelim2 4222  dom2d 4404  rankr1lem 4673  unidom 4808  alephnbtwn 4868  alephval2 4902  axpowndlem3 4951  distrlem4pr 5130  sqgt0sr 5215  suppsr3 5224  renegcl 5416  xrletrit 5561  letrit 5620  redivcl 5798  nnge1t 5943  nnleltp1t 5954  nnsub 5956  avglet 6044  uzind2 6206  uzwo4OLD 6210  nn0ind-raph 6214  zbtwnre 6221  qsqueeze 6280  monoord 6294  om2uzf1o 6301  icounlem 6412  uzwo 6455  uzwoOLD 6456  cvg2 6922  facdivt 6942  facwordit 6944  caucvg 7163  ser1f0 7170  infcvglem3 7223  znnenlem 7501  infpnlem1 7506  infxpidmlem5 7556  infxpidmlem11 7562  qdensere 7751  metxp 7834  metcnp 7887  cmsss 7997  bcthlem18 8016  bcthlem28 8026  minveclem25 8569  spwval2 8653  efifolem5 8726  efif1lem4 8733  hlimcaui 9106  occllem6 9178  shmods 9362  nmcopexlem6 9956  nmcfnexlem6 9985  rnbra 10040  bra11 10041  atcvat 10313  atcvat2 10314  irredlem4 10320  atmd2 10327  sumdmdlem 10345  oprabvaligg 10440  cdrci 10494  iintlem1 10632

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