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  1809  eqreu  2953  onsucsssucr  4542  ordsucunielexmid  4564  ovi3  6057  tfrlem9  6374  dom2lem  6828  distrlem4prl  7646  distrlem4pru  7647  recexprlemm  7686  caucvgprlem1  7741  caucvgprprlemexb  7769  aptisr  7841  map2psrprg  7867  renegcl  8282  addid0  8394  remulext2  8621  mulext1  8633  apmul1  8809  nnge1  9007  0mnnnnn0  9275  nn0lt2  9401  zneo  9421  uzind2  9432  fzind  9435  nn0ind-raph  9437  ledivge1le  9795  elfzmlbp  10201  difelfznle  10204  elfzodifsumelfzo  10271  ssfzo12  10294  flqeqceilz  10392  addmodlteq  10472  uzsinds  10518  qsqeqor  10724  facdiv  10812  facwordi  10814  bcpasc  10840  addcn2  11456  mulcn2  11458  climrecvg1n  11494  odd2np1  12017  oddge22np1  12025  gcdaddm  12124  algcvgblem  12190  cncongr1  12244  pcdvdsb  12461  pcaddlem  12480  infpnlem1  12500  prmunb  12503  imasaddfnlemg  12900  f1ghm0to0  13345  ghmf1  13346  imasring  13563  subrgdvds  13734  aprcotr  13784  quscrng  14032  metss2lem  14676  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215  lgseisenlem2  15228  2sqlem6  15277