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  6594  dom2lem  7062  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  9738  zneo  9758  uzind2  9769  fzind  9772  nn0ind-raph  9774  ledivge1le  10144  elfzmlbp  10556  difelfznle  10559  elfzodifsumelfzo  10636  ssfzo12  10659  flqeqceilz  10776  addmodlteq  10856  uzsinds  10902  qsqeqor  11108  facdiv  11198  facwordi  11200  bcpasc  11226  ccatsymb  11392  swrdsbslen  11460  swrdspsleq  11461  swrdlsw  11463  swrdswrdlem  11498  swrdccatin1  11519  pfxccatin12lem3  11526  swrdccat  11529  pfxccat3a  11532  addcn2  12101  mulcn2  12103  climrecvg1n  12139  odd2np1  12665  oddge22np1  12673  bitsfzo  12747  gcdaddm  12786  algcvgblem  12852  cncongr1  12906  pcdvdsb  13128  pcaddlem  13147  infpnlem1  13167  prmunb  13170  imasaddfnlemg  13694  f1ghm0to0  14134  ghmf1  14135  gsumcom2fi  14275  imasring  14478  subrgdvds  14652  aprcotr  14706  quscrng  14979  rnasclassa  15147  metss2lem  15723  pellexlem1  16229  ppiqeq0  16280  chtqub  16296  bposlem6  16316  gausslemma2dlem0i  16381  gausslemma2dlem1a  16382  lgseisenlem2  16395  2sqlem6  16444  incistruhgr  16536  wlk1walkdom  16805  wlkv0  16815  clwwlkccatlem  16846