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  4656  ordsucunielexmid  4678  riotaeqimp  6063  ovi3  6226  suppssrst  6501  suppssrgst  6502  tfrlem9  6590  dom2lem  7058  distrlem4prl  7951  distrlem4pru  7952  recexprlemm  7991  caucvgprlem1  8046  caucvgprprlemexb  8074  aptisr  8146  map2psrprg  8172  renegcl  8587  addid0  8699  remulext2  8928  mulext1  8940  apmul1  9118  nnge1  9327  0mnnnnn0  9595  nn0lt2  9727  zneo  9747  uzind2  9758  fzind  9761  nn0ind-raph  9763  ledivge1le  10127  elfzmlbp  10539  difelfznle  10542  elfzodifsumelfzo  10619  ssfzo12  10642  flqeqceilz  10755  addmodlteq  10835  uzsinds  10881  qsqeqor  11087  facdiv  11176  facwordi  11178  bcpasc  11204  ccatsymb  11370  swrdsbslen  11438  swrdspsleq  11439  swrdlsw  11441  swrdswrdlem  11476  swrdccatin1  11497  pfxccatin12lem3  11504  swrdccat  11507  pfxccat3a  11510  addcn2  12076  mulcn2  12078  climrecvg1n  12114  odd2np1  12640  oddge22np1  12648  bitsfzo  12722  gcdaddm  12761  algcvgblem  12827  cncongr1  12881  pcdvdsb  13099  pcaddlem  13118  infpnlem1  13138  prmunb  13141  imasaddfnlemg  13635  f1ghm0to0  14075  ghmf1  14076  imasring  14369  subrgdvds  14543  aprcotr  14597  quscrng  14870  rnasclassa  15038  metss2lem  15598  pellexlem1  16091  gausslemma2dlem0i  16176  gausslemma2dlem1a  16177  lgseisenlem2  16190  2sqlem6  16239  incistruhgr  16331  wlk1walkdom  16600  wlkv0  16610  clwwlkccatlem  16641