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  1798  eqreu  2931  onsucsssucr  4510  ordsucunielexmid  4532  ovi3  6014  tfrlem9  6323  dom2lem  6775  distrlem4prl  7586  distrlem4pru  7587  recexprlemm  7626  caucvgprlem1  7681  caucvgprprlemexb  7709  aptisr  7781  map2psrprg  7807  renegcl  8221  addid0  8333  remulext2  8560  mulext1  8572  apmul1  8748  nnge1  8945  0mnnnnn0  9211  nn0lt2  9337  zneo  9357  uzind2  9368  fzind  9371  nn0ind-raph  9373  ledivge1le  9729  elfzmlbp  10135  difelfznle  10138  elfzodifsumelfzo  10204  ssfzo12  10227  flqeqceilz  10321  addmodlteq  10401  uzsinds  10445  qsqeqor  10634  facdiv  10721  facwordi  10723  bcpasc  10749  addcn2  11321  mulcn2  11323  climrecvg1n  11359  odd2np1  11881  oddge22np1  11889  gcdaddm  11988  algcvgblem  12052  cncongr1  12106  pcdvdsb  12322  pcaddlem  12341  infpnlem1  12360  prmunb  12363  imasaddfnlemg  12741  subrgdvds  13362  aprcotr  13381  metss2lem  14137  lgseisenlem2  14591  2sqlem6  14607