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  1812  eqreu  2956  onsucsssucr  4546  ordsucunielexmid  4568  ovi3  6064  tfrlem9  6386  dom2lem  6840  distrlem4prl  7668  distrlem4pru  7669  recexprlemm  7708  caucvgprlem1  7763  caucvgprprlemexb  7791  aptisr  7863  map2psrprg  7889  renegcl  8304  addid0  8416  remulext2  8644  mulext1  8656  apmul1  8832  nnge1  9030  0mnnnnn0  9298  nn0lt2  9424  zneo  9444  uzind2  9455  fzind  9458  nn0ind-raph  9460  ledivge1le  9818  elfzmlbp  10224  difelfznle  10227  elfzodifsumelfzo  10294  ssfzo12  10317  flqeqceilz  10427  addmodlteq  10507  uzsinds  10553  qsqeqor  10759  facdiv  10847  facwordi  10849  bcpasc  10875  addcn2  11492  mulcn2  11494  climrecvg1n  11530  odd2np1  12055  oddge22np1  12063  bitsfzo  12137  gcdaddm  12176  algcvgblem  12242  cncongr1  12296  pcdvdsb  12514  pcaddlem  12533  infpnlem1  12553  prmunb  12556  imasaddfnlemg  13016  f1ghm0to0  13478  ghmf1  13479  imasring  13696  subrgdvds  13867  aprcotr  13917  quscrng  14165  metss2lem  14817  gausslemma2dlem0i  15382  gausslemma2dlem1a  15383  lgseisenlem2  15396  2sqlem6  15445