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  1822  eqreu  2972  onsucsssucr  4575  ordsucunielexmid  4597  ovi3  6106  tfrlem9  6428  dom2lem  6886  distrlem4prl  7732  distrlem4pru  7733  recexprlemm  7772  caucvgprlem1  7827  caucvgprprlemexb  7855  aptisr  7927  map2psrprg  7953  renegcl  8368  addid0  8480  remulext2  8708  mulext1  8720  apmul1  8896  nnge1  9094  0mnnnnn0  9362  nn0lt2  9489  zneo  9509  uzind2  9520  fzind  9523  nn0ind-raph  9525  ledivge1le  9883  elfzmlbp  10289  difelfznle  10292  elfzodifsumelfzo  10367  ssfzo12  10390  flqeqceilz  10500  addmodlteq  10580  uzsinds  10626  qsqeqor  10832  facdiv  10920  facwordi  10922  bcpasc  10948  ccatsymb  11096  swrdsbslen  11157  swrdspsleq  11158  swrdlsw  11160  swrdswrdlem  11195  swrdccatin1  11216  pfxccatin12lem3  11223  swrdccat  11226  pfxccat3a  11229  addcn2  11736  mulcn2  11738  climrecvg1n  11774  odd2np1  12299  oddge22np1  12307  bitsfzo  12381  gcdaddm  12420  algcvgblem  12486  cncongr1  12540  pcdvdsb  12758  pcaddlem  12777  infpnlem1  12797  prmunb  12800  imasaddfnlemg  13261  f1ghm0to0  13723  ghmf1  13724  imasring  13941  subrgdvds  14112  aprcotr  14162  quscrng  14410  metss2lem  15084  gausslemma2dlem0i  15649  gausslemma2dlem1a  15650  lgseisenlem2  15663  2sqlem6  15712  incistruhgr  15801