Theorem sylbird 180

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

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  3imtr3d 420  hbsbcg 1445  limom 2387  nnsuc 2389  findsg 2398  tfindsg 2402  tfindsg2 2403  tfrlem9 2957  oe0lem 3121  oa00 3161  dom2d 3307  rankr1lem 3517  alephnbtwn 3674  axpowndlem3 3745  distrlem4pr 3924  sqgt0sr 4009  suppsr3 4018  renegcl 4171  redivcl 4274  nnge1t 4439  nnleltp1t 4448  nnsub 4450  uzwo 4605  nnwoOLD 4608  nn0ind 4612  zbtwnre 4619  om2uzf1o 4656  znnenlem 4929  infxpidmlem5 4937  infxpidmlem11 4943  hlimcaui 5141  occllem6 5185  shmods 5363  atcvat 5771  atcvat2 5772  sumdmdlem 5786

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

This theorem depends on definitions:  df-bi 128

metamath.org