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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3d  202  drex1  1851  eqreu  3018  onsucsssucr  4658  ordsucunielexmid  4680  riotaeqimp  6066  ovi3  6229  suppssrst  6505  suppssrgst  6506  tfrlem9  6595  dom2lem  7064  distrlem4prl  7957  distrlem4pru  7958  recexprlemm  7997  caucvgprlem1  8052  caucvgprprlemexb  8080  aptisr  8152  map2psrprg  8178  renegcl  8594  addid0  8706  remulext2  8936  mulext1  8948  apmul1  9126  nnge1  9336  0mnnnnn0  9606  nn0lt2  9736  zneo  9757  uzind2  9768  fzind  9771  nn0ind-raph  9773  ledivge1le  10143  elfzmlbp  10555  difelfznle  10558  elfzodifsumelfzo  10635  ssfzo12  10658  flqeqceilz  10775  addmodlteq  10855  uzsinds  10901  qsqeqor  11107  facdiv  11197  facwordi  11199  bcpasc  11225  ccatsymb  11391  swrdsbslen  11459  swrdspsleq  11460  swrdlsw  11462  swrdswrdlem  11497  swrdccatin1  11518  pfxccatin12lem3  11525  swrdccat  11528  pfxccat3a  11531  addcn2  12100  mulcn2  12102  climrecvg1n  12138  odd2np1  12664  oddge22np1  12672  bitsfzo  12746  gcdaddm  12785  algcvgblem  12851  cncongr1  12905  pcdvdsb  13127  pcaddlem  13146  infpnlem1  13166  prmunb  13169  imasaddfnlemg  13693  f1ghm0to0  14133  ghmf1  14134  gsumcom2fi  14274  imasring  14477  subrgdvds  14651  aprcotr  14705  quscrng  14978  rnasclassa  15146  metss2lem  15740  pellexlem1  16246  ppiqeq0  16297  chtqub  16313  bposlem6  16333  gausslemma2dlem0i  16398  gausslemma2dlem1a  16399  lgseisenlem2  16412  2sqlem6  16461  incistruhgr  16553  wlk1walkdom  16822  wlkv0  16832  clwwlkccatlem  16863