Theorem sylbird 169

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

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

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3d  201  drex1  1752  eqreu  2845  onsucsssucr  4385  ordsucunielexmid  4406  ovi3  5861  tfrlem9  6170  dom2lem  6620  distrlem4prl  7340  distrlem4pru  7341  recexprlemm  7380  caucvgprlem1  7435  caucvgprprlemexb  7463  aptisr  7521  renegcl  7946  addid0  8054  remulext2  8280  mulext1  8292  apmul1  8461  nnge1  8653  0mnnnnn0  8913  nn0lt2  9036  zneo  9056  uzind2  9067  fzind  9070  nn0ind-raph  9072  ledivge1le  9412  elfzmlbp  9802  difelfznle  9805  elfzodifsumelfzo  9871  ssfzo12  9894  flqeqceilz  9984  addmodlteq  10064  uzsinds  10108  facdiv  10377  facwordi  10379  bcpasc  10405  addcn2  10971  mulcn2  10973  climrecvg1n  11009  odd2np1  11418  oddge22np1  11426  gcdaddm  11520  algcvgblem  11576  cncongr1  11630  metss2lem  12486