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  1847  eqreu  3009  onsucsssucr  4631  ordsucunielexmid  4653  riotaeqimp  6028  ovi3  6191  suppssrst  6461  suppssrgst  6462  tfrlem9  6550  dom2lem  7011  distrlem4prl  7899  distrlem4pru  7900  recexprlemm  7939  caucvgprlem1  7994  caucvgprprlemexb  8022  aptisr  8094  map2psrprg  8120  renegcl  8534  addid0  8646  remulext2  8874  mulext1  8886  apmul1  9062  nnge1  9260  0mnnnnn0  9528  nn0lt2  9659  zneo  9679  uzind2  9690  fzind  9693  nn0ind-raph  9695  ledivge1le  10059  elfzmlbp  10466  difelfznle  10469  elfzodifsumelfzo  10546  ssfzo12  10569  flqeqceilz  10680  addmodlteq  10760  uzsinds  10806  qsqeqor  11012  facdiv  11100  facwordi  11102  bcpasc  11128  ccatsymb  11290  swrdsbslen  11358  swrdspsleq  11359  swrdlsw  11361  swrdswrdlem  11396  swrdccatin1  11417  pfxccatin12lem3  11424  swrdccat  11427  pfxccat3a  11430  addcn2  11995  mulcn2  11997  climrecvg1n  12033  odd2np1  12559  oddge22np1  12567  bitsfzo  12641  gcdaddm  12680  algcvgblem  12746  cncongr1  12800  pcdvdsb  13018  pcaddlem  13037  infpnlem1  13057  prmunb  13060  imasaddfnlemg  13527  f1ghm0to0  13989  ghmf1  13990  imasring  14208  subrgdvds  14380  aprcotr  14431  quscrng  14681  metss2lem  15362  pellexlem1  15845  gausslemma2dlem0i  15930  gausslemma2dlem1a  15931  lgseisenlem2  15944  2sqlem6  15993  incistruhgr  16085  wlk1walkdom  16354  wlkv0  16364  clwwlkccatlem  16395