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  8588  addid0  8700  remulext2  8930  mulext1  8942  apmul1  9120  nnge1  9329  0mnnnnn0  9599  nn0lt2  9731  zneo  9751  uzind2  9762  fzind  9765  nn0ind-raph  9767  ledivge1le  10137  elfzmlbp  10549  difelfznle  10552  elfzodifsumelfzo  10629  ssfzo12  10652  flqeqceilz  10768  addmodlteq  10848  uzsinds  10894  qsqeqor  11100  facdiv  11190  facwordi  11192  bcpasc  11218  ccatsymb  11384  swrdsbslen  11452  swrdspsleq  11453  swrdlsw  11455  swrdswrdlem  11490  swrdccatin1  11511  pfxccatin12lem3  11518  swrdccat  11521  pfxccat3a  11524  addcn2  12092  mulcn2  12094  climrecvg1n  12130  odd2np1  12656  oddge22np1  12664  bitsfzo  12738  gcdaddm  12777  algcvgblem  12843  cncongr1  12897  pcdvdsb  13119  pcaddlem  13138  infpnlem1  13158  prmunb  13161  imasaddfnlemg  13684  f1ghm0to0  14124  ghmf1  14125  imasring  14418  subrgdvds  14592  aprcotr  14646  quscrng  14919  rnasclassa  15087  metss2lem  15647  pellexlem1  16148  ppiqeq0  16182  gausslemma2dlem0i  16274  gausslemma2dlem1a  16275  lgseisenlem2  16288  2sqlem6  16337  incistruhgr  16429  wlk1walkdom  16698  wlkv0  16708  clwwlkccatlem  16739