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  1847  eqreu  3012  onsucsssucr  4636  ordsucunielexmid  4658  riotaeqimp  6036  ovi3  6199  suppssrst  6474  suppssrgst  6475  tfrlem9  6563  dom2lem  7024  distrlem4prl  7915  distrlem4pru  7916  recexprlemm  7955  caucvgprlem1  8010  caucvgprprlemexb  8038  aptisr  8110  map2psrprg  8136  renegcl  8550  addid0  8662  remulext2  8891  mulext1  8903  apmul1  9079  nnge1  9277  0mnnnnn0  9545  nn0lt2  9677  zneo  9697  uzind2  9708  fzind  9711  nn0ind-raph  9713  ledivge1le  10077  elfzmlbp  10488  difelfznle  10491  elfzodifsumelfzo  10568  ssfzo12  10591  flqeqceilz  10704  addmodlteq  10784  uzsinds  10830  qsqeqor  11036  facdiv  11125  facwordi  11127  bcpasc  11153  ccatsymb  11315  swrdsbslen  11383  swrdspsleq  11384  swrdlsw  11386  swrdswrdlem  11421  swrdccatin1  11442  pfxccatin12lem3  11449  swrdccat  11452  pfxccat3a  11455  addcn2  12020  mulcn2  12022  climrecvg1n  12058  odd2np1  12584  oddge22np1  12592  bitsfzo  12666  gcdaddm  12705  algcvgblem  12771  cncongr1  12825  pcdvdsb  13043  pcaddlem  13062  infpnlem1  13082  prmunb  13085  imasaddfnlemg  13578  f1ghm0to0  14025  ghmf1  14026  imasring  14307  subrgdvds  14481  aprcotr  14535  quscrng  14807  metss2lem  15488  pellexlem1  15971  gausslemma2dlem0i  16056  gausslemma2dlem1a  16057  lgseisenlem2  16070  2sqlem6  16119  incistruhgr  16211  wlk1walkdom  16480  wlkv0  16490  clwwlkccatlem  16521