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  1844  eqreu  2995  onsucsssucr  4601  ordsucunielexmid  4623  riotaeqimp  5985  ovi3  6148  tfrlem9  6471  dom2lem  6931  distrlem4prl  7782  distrlem4pru  7783  recexprlemm  7822  caucvgprlem1  7877  caucvgprprlemexb  7905  aptisr  7977  map2psrprg  8003  renegcl  8418  addid0  8530  remulext2  8758  mulext1  8770  apmul1  8946  nnge1  9144  0mnnnnn0  9412  nn0lt2  9539  zneo  9559  uzind2  9570  fzind  9573  nn0ind-raph  9575  ledivge1le  9934  elfzmlbp  10340  difelfznle  10343  elfzodifsumelfzo  10419  ssfzo12  10442  flqeqceilz  10552  addmodlteq  10632  uzsinds  10678  qsqeqor  10884  facdiv  10972  facwordi  10974  bcpasc  11000  ccatsymb  11150  swrdsbslen  11213  swrdspsleq  11214  swrdlsw  11216  swrdswrdlem  11251  swrdccatin1  11272  pfxccatin12lem3  11279  swrdccat  11282  pfxccat3a  11285  addcn2  11836  mulcn2  11838  climrecvg1n  11874  odd2np1  12399  oddge22np1  12407  bitsfzo  12481  gcdaddm  12520  algcvgblem  12586  cncongr1  12640  pcdvdsb  12858  pcaddlem  12877  infpnlem1  12897  prmunb  12900  imasaddfnlemg  13362  f1ghm0to0  13824  ghmf1  13825  imasring  14042  subrgdvds  14214  aprcotr  14264  quscrng  14512  metss2lem  15186  gausslemma2dlem0i  15751  gausslemma2dlem1a  15752  lgseisenlem2  15765  2sqlem6  15814  incistruhgr  15905  wlk1walkdom  16100  wlkv0  16110  clwwlkccatlem  16137