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  1851  eqreu  3018  onsucsssucr  4651  ordsucunielexmid  4673  riotaeqimp  6053  ovi3  6216  suppssrst  6491  suppssrgst  6492  tfrlem9  6580  dom2lem  7048  distrlem4prl  7941  distrlem4pru  7942  recexprlemm  7981  caucvgprlem1  8036  caucvgprprlemexb  8064  aptisr  8136  map2psrprg  8162  renegcl  8577  addid0  8689  remulext2  8918  mulext1  8930  apmul1  9108  nnge1  9306  0mnnnnn0  9574  nn0lt2  9706  zneo  9726  uzind2  9737  fzind  9740  nn0ind-raph  9742  ledivge1le  10106  elfzmlbp  10517  difelfznle  10520  elfzodifsumelfzo  10597  ssfzo12  10620  flqeqceilz  10733  addmodlteq  10813  uzsinds  10859  qsqeqor  11065  facdiv  11154  facwordi  11156  bcpasc  11182  ccatsymb  11348  swrdsbslen  11416  swrdspsleq  11417  swrdlsw  11419  swrdswrdlem  11454  swrdccatin1  11475  pfxccatin12lem3  11482  swrdccat  11485  pfxccat3a  11488  addcn2  12054  mulcn2  12056  climrecvg1n  12092  odd2np1  12618  oddge22np1  12626  bitsfzo  12700  gcdaddm  12739  algcvgblem  12805  cncongr1  12859  pcdvdsb  13077  pcaddlem  13096  infpnlem1  13116  prmunb  13119  imasaddfnlemg  13612  f1ghm0to0  14052  ghmf1  14053  imasring  14342  subrgdvds  14516  aprcotr  14570  quscrng  14842  metss2lem  15521  pellexlem1  16005  gausslemma2dlem0i  16090  gausslemma2dlem1a  16091  lgseisenlem2  16104  2sqlem6  16153  incistruhgr  16245  wlk1walkdom  16514  wlkv0  16524  clwwlkccatlem  16555