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  1846  eqreu  2999  onsucsssucr  4613  ordsucunielexmid  4635  riotaeqimp  6006  ovi3  6169  suppssrst  6439  suppssrgst  6440  tfrlem9  6528  dom2lem  6988  distrlem4prl  7847  distrlem4pru  7848  recexprlemm  7887  caucvgprlem1  7942  caucvgprprlemexb  7970  aptisr  8042  map2psrprg  8068  renegcl  8482  addid0  8594  remulext2  8822  mulext1  8834  apmul1  9010  nnge1  9208  0mnnnnn0  9476  nn0lt2  9605  zneo  9625  uzind2  9636  fzind  9639  nn0ind-raph  9641  ledivge1le  10005  elfzmlbp  10412  difelfznle  10415  elfzodifsumelfzo  10492  ssfzo12  10515  flqeqceilz  10626  addmodlteq  10706  uzsinds  10752  qsqeqor  10958  facdiv  11046  facwordi  11048  bcpasc  11074  ccatsymb  11228  swrdsbslen  11296  swrdspsleq  11297  swrdlsw  11299  swrdswrdlem  11334  swrdccatin1  11355  pfxccatin12lem3  11362  swrdccat  11365  pfxccat3a  11368  addcn2  11933  mulcn2  11935  climrecvg1n  11971  odd2np1  12497  oddge22np1  12505  bitsfzo  12579  gcdaddm  12618  algcvgblem  12684  cncongr1  12738  pcdvdsb  12956  pcaddlem  12975  infpnlem1  12995  prmunb  12998  imasaddfnlemg  13460  f1ghm0to0  13922  ghmf1  13923  imasring  14141  subrgdvds  14313  aprcotr  14364  quscrng  14612  metss2lem  15291  pellexlem1  15774  gausslemma2dlem0i  15859  gausslemma2dlem1a  15860  lgseisenlem2  15873  2sqlem6  15922  incistruhgr  16014  wlk1walkdom  16283  wlkv0  16293  clwwlkccatlem  16324