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  1820  eqreu  2964  onsucsssucr  4555  ordsucunielexmid  4577  ovi3  6073  tfrlem9  6395  dom2lem  6849  distrlem4prl  7679  distrlem4pru  7680  recexprlemm  7719  caucvgprlem1  7774  caucvgprprlemexb  7802  aptisr  7874  map2psrprg  7900  renegcl  8315  addid0  8427  remulext2  8655  mulext1  8667  apmul1  8843  nnge1  9041  0mnnnnn0  9309  nn0lt2  9436  zneo  9456  uzind2  9467  fzind  9470  nn0ind-raph  9472  ledivge1le  9830  elfzmlbp  10236  difelfznle  10239  elfzodifsumelfzo  10311  ssfzo12  10334  flqeqceilz  10444  addmodlteq  10524  uzsinds  10570  qsqeqor  10776  facdiv  10864  facwordi  10866  bcpasc  10892  ccatsymb  11033  addcn2  11540  mulcn2  11542  climrecvg1n  11578  odd2np1  12103  oddge22np1  12111  bitsfzo  12185  gcdaddm  12224  algcvgblem  12290  cncongr1  12344  pcdvdsb  12562  pcaddlem  12581  infpnlem1  12601  prmunb  12604  imasaddfnlemg  13064  f1ghm0to0  13526  ghmf1  13527  imasring  13744  subrgdvds  13915  aprcotr  13965  quscrng  14213  metss2lem  14887  gausslemma2dlem0i  15452  gausslemma2dlem1a  15453  lgseisenlem2  15466  2sqlem6  15515