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  2876  onsucsssucr  4425  ordsucunielexmid  4446  ovi3  5907  tfrlem9  6216  dom2lem  6666  distrlem4prl  7392  distrlem4pru  7393  recexprlemm  7432  caucvgprlem1  7487  caucvgprprlemexb  7515  aptisr  7587  map2psrprg  7613  renegcl  8023  addid0  8135  remulext2  8362  mulext1  8374  apmul1  8548  nnge1  8743  0mnnnnn0  9009  nn0lt2  9132  zneo  9152  uzind2  9163  fzind  9166  nn0ind-raph  9168  ledivge1le  9513  elfzmlbp  9909  difelfznle  9912  elfzodifsumelfzo  9978  ssfzo12  10001  flqeqceilz  10091  addmodlteq  10171  uzsinds  10215  facdiv  10484  facwordi  10486  bcpasc  10512  addcn2  11079  mulcn2  11081  climrecvg1n  11117  odd2np1  11570  oddge22np1  11578  gcdaddm  11672  algcvgblem  11730  cncongr1  11784  metss2lem  12666