Theorem sylbird 170

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 158	. 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 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3d  202  drex1  1812  eqreu  2956  onsucsssucr  4545  ordsucunielexmid  4567  ovi3  6060  tfrlem9  6377  dom2lem  6831  distrlem4prl  7651  distrlem4pru  7652  recexprlemm  7691  caucvgprlem1  7746  caucvgprprlemexb  7774  aptisr  7846  map2psrprg  7872  renegcl  8287  addid0  8399  remulext2  8627  mulext1  8639  apmul1  8815  nnge1  9013  0mnnnnn0  9281  nn0lt2  9407  zneo  9427  uzind2  9438  fzind  9441  nn0ind-raph  9443  ledivge1le  9801  elfzmlbp  10207  difelfznle  10210  elfzodifsumelfzo  10277  ssfzo12  10300  flqeqceilz  10410  addmodlteq  10490  uzsinds  10536  qsqeqor  10742  facdiv  10830  facwordi  10832  bcpasc  10858  addcn2  11475  mulcn2  11477  climrecvg1n  11513  odd2np1  12038  oddge22np1  12046  bitsfzo  12119  gcdaddm  12151  algcvgblem  12217  cncongr1  12271  pcdvdsb  12489  pcaddlem  12508  infpnlem1  12528  prmunb  12531  imasaddfnlemg  12957  f1ghm0to0  13402  ghmf1  13403  imasring  13620  subrgdvds  13791  aprcotr  13841  quscrng  14089  metss2lem  14733  gausslemma2dlem0i  15298  gausslemma2dlem1a  15299  lgseisenlem2  15312  2sqlem6  15361