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  1844  eqreu  2996  onsucsssucr  4605  ordsucunielexmid  4627  riotaeqimp  5991  ovi3  6154  tfrlem9  6480  dom2lem  6940  distrlem4prl  7794  distrlem4pru  7795  recexprlemm  7834  caucvgprlem1  7889  caucvgprprlemexb  7917  aptisr  7989  map2psrprg  8015  renegcl  8430  addid0  8542  remulext2  8770  mulext1  8782  apmul1  8958  nnge1  9156  0mnnnnn0  9424  nn0lt2  9551  zneo  9571  uzind2  9582  fzind  9585  nn0ind-raph  9587  ledivge1le  9951  elfzmlbp  10357  difelfznle  10360  elfzodifsumelfzo  10436  ssfzo12  10459  flqeqceilz  10570  addmodlteq  10650  uzsinds  10696  qsqeqor  10902  facdiv  10990  facwordi  10992  bcpasc  11018  ccatsymb  11169  swrdsbslen  11237  swrdspsleq  11238  swrdlsw  11240  swrdswrdlem  11275  swrdccatin1  11296  pfxccatin12lem3  11303  swrdccat  11306  pfxccat3a  11309  addcn2  11861  mulcn2  11863  climrecvg1n  11899  odd2np1  12424  oddge22np1  12432  bitsfzo  12506  gcdaddm  12545  algcvgblem  12611  cncongr1  12665  pcdvdsb  12883  pcaddlem  12902  infpnlem1  12922  prmunb  12925  imasaddfnlemg  13387  f1ghm0to0  13849  ghmf1  13850  imasring  14067  subrgdvds  14239  aprcotr  14289  quscrng  14537  metss2lem  15211  gausslemma2dlem0i  15776  gausslemma2dlem1a  15777  lgseisenlem2  15790  2sqlem6  15839  incistruhgr  15931  wlk1walkdom  16156  wlkv0  16166  clwwlkccatlem  16195