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  2998  onsucsssucr  4607  ordsucunielexmid  4629  riotaeqimp  5996  ovi3  6159  tfrlem9  6485  dom2lem  6945  distrlem4prl  7804  distrlem4pru  7805  recexprlemm  7844  caucvgprlem1  7899  caucvgprprlemexb  7927  aptisr  7999  map2psrprg  8025  renegcl  8440  addid0  8552  remulext2  8780  mulext1  8792  apmul1  8968  nnge1  9166  0mnnnnn0  9434  nn0lt2  9561  zneo  9581  uzind2  9592  fzind  9595  nn0ind-raph  9597  ledivge1le  9961  elfzmlbp  10367  difelfznle  10370  elfzodifsumelfzo  10447  ssfzo12  10470  flqeqceilz  10581  addmodlteq  10661  uzsinds  10707  qsqeqor  10913  facdiv  11001  facwordi  11003  bcpasc  11029  ccatsymb  11183  swrdsbslen  11251  swrdspsleq  11252  swrdlsw  11254  swrdswrdlem  11289  swrdccatin1  11310  pfxccatin12lem3  11317  swrdccat  11320  pfxccat3a  11323  addcn2  11888  mulcn2  11890  climrecvg1n  11926  odd2np1  12452  oddge22np1  12460  bitsfzo  12534  gcdaddm  12573  algcvgblem  12639  cncongr1  12693  pcdvdsb  12911  pcaddlem  12930  infpnlem1  12950  prmunb  12953  imasaddfnlemg  13415  f1ghm0to0  13877  ghmf1  13878  imasring  14096  subrgdvds  14268  aprcotr  14318  quscrng  14566  metss2lem  15240  gausslemma2dlem0i  15805  gausslemma2dlem1a  15806  lgseisenlem2  15819  2sqlem6  15868  incistruhgr  15960  wlk1walkdom  16229  wlkv0  16239  clwwlkccatlem  16270