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  7952  distrlem4pru  7953  recexprlemm  7992  caucvgprlem1  8047  caucvgprprlemexb  8075  aptisr  8147  map2psrprg  8173  renegcl  8589  addid0  8701  remulext2  8931  mulext1  8943  apmul1  9121  nnge1  9330  0mnnnnn0  9600  nn0lt2  9732  zneo  9752  uzind2  9763  fzind  9766  nn0ind-raph  9768  ledivge1le  10138  elfzmlbp  10550  difelfznle  10553  elfzodifsumelfzo  10630  ssfzo12  10653  flqeqceilz  10770  addmodlteq  10850  uzsinds  10896  qsqeqor  11102  facdiv  11192  facwordi  11194  bcpasc  11220  ccatsymb  11386  swrdsbslen  11454  swrdspsleq  11455  swrdlsw  11457  swrdswrdlem  11492  swrdccatin1  11513  pfxccatin12lem3  11520  swrdccat  11523  pfxccat3a  11526  addcn2  12095  mulcn2  12097  climrecvg1n  12133  odd2np1  12659  oddge22np1  12667  bitsfzo  12741  gcdaddm  12780  algcvgblem  12846  cncongr1  12900  pcdvdsb  13122  pcaddlem  13141  infpnlem1  13161  prmunb  13164  imasaddfnlemg  13688  f1ghm0to0  14128  ghmf1  14129  imasring  14453  subrgdvds  14627  aprcotr  14681  quscrng  14954  rnasclassa  15122  metss2lem  15689  pellexlem1  16190  ppiqeq0  16241  chtqub  16257  bposlem6  16277  gausslemma2dlem0i  16342  gausslemma2dlem1a  16343  lgseisenlem2  16356  2sqlem6  16405  incistruhgr  16497  wlk1walkdom  16766  wlkv0  16776  clwwlkccatlem  16807