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-mp 5  ax-1 6  ax-2 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  1770  eqreu  2871  onsucsssucr  4420  ordsucunielexmid  4441  ovi3  5900  tfrlem9  6209  dom2lem  6659  distrlem4prl  7385  distrlem4pru  7386  recexprlemm  7425  caucvgprlem1  7480  caucvgprprlemexb  7508  aptisr  7580  map2psrprg  7606  renegcl  8016  addid0  8128  remulext2  8355  mulext1  8367  apmul1  8541  nnge1  8736  0mnnnnn0  9002  nn0lt2  9125  zneo  9145  uzind2  9156  fzind  9159  nn0ind-raph  9161  ledivge1le  9506  elfzmlbp  9902  difelfznle  9905  elfzodifsumelfzo  9971  ssfzo12  9994  flqeqceilz  10084  addmodlteq  10164  uzsinds  10208  facdiv  10477  facwordi  10479  bcpasc  10505  addcn2  11072  mulcn2  11074  climrecvg1n  11110  odd2np1  11559  oddge22np1  11567  gcdaddm  11661  algcvgblem  11719  cncongr1  11773  metss2lem  12655