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 540  hbsbc1g 1938  ordsssuc2 3049  limom 3136  nnsuc 3138  findsg 3147  tfindsg 3152  tfindsg2 3153  tfrlem9 3904  oe0lem 4136  oa00 4177  omwordi 4186  om00 4190  omass 4195  oelim2 4206  dom2d 4385  rankr1lem 4645  unidom 4780  alephnbtwn 4840  alephval2 4874  axpowndlem3 4923  distrlem4pr 5102  sqgt0sr 5187  suppsr3 5196  renegcl 5388  xrletrit 5534  letrit 5594  redivcl 5754  nnge1t 5891  nnleltp1t 5901  nnsub 5903  avglet 5991  uzind2 6154  uzwo4OLD 6158  nn0ind-raph 6162  zbtwnre 6169  qsqueeze 6218  monoord 6231  om2uzf1o 6238  icounlem 6345  uzwo 6387  uzwoOLD 6388  cvg2 6859  facdivt 6879  facwordit 6881  caucvg 7099  ser1f0 7106  infcvglem3 7158  znnenlem 7443  znnenlemOLD 7444  infpnlem1 7449  infxpidmlem5 7499  infxpidmlem11 7505  qdensere 7691  metxp 7774  metcnp 7826  cmsss 7931  bcthlem18 7950  bcthlem28 7960  minveclem25 8500  spwval2 8577  efifolem5 8641  efif1lem4 8648  hlimcaui 9027  occllem6 9094  shmods 9277  nmcopexlem6 9871  nmcfnexlem6 9900  rnbra 9953  bra11 9954  atcvat 10221  atcvat2 10222  irredlem4 10228  atmd2 10235  sumdmdlem 10252  oprabvaligg 10341  cdrci 10381  iintlem1 10476

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