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  2995  onsucsssucr  4600  ordsucunielexmid  4622  riotaeqimp  5978  ovi3  6141  tfrlem9  6463  dom2lem  6921  distrlem4prl  7767  distrlem4pru  7768  recexprlemm  7807  caucvgprlem1  7862  caucvgprprlemexb  7890  aptisr  7962  map2psrprg  7988  renegcl  8403  addid0  8515  remulext2  8743  mulext1  8755  apmul1  8931  nnge1  9129  0mnnnnn0  9397  nn0lt2  9524  zneo  9544  uzind2  9555  fzind  9558  nn0ind-raph  9560  ledivge1le  9918  elfzmlbp  10324  difelfznle  10327  elfzodifsumelfzo  10402  ssfzo12  10425  flqeqceilz  10535  addmodlteq  10615  uzsinds  10661  qsqeqor  10867  facdiv  10955  facwordi  10957  bcpasc  10983  ccatsymb  11132  swrdsbslen  11193  swrdspsleq  11194  swrdlsw  11196  swrdswrdlem  11231  swrdccatin1  11252  pfxccatin12lem3  11259  swrdccat  11262  pfxccat3a  11265  addcn2  11816  mulcn2  11818  climrecvg1n  11854  odd2np1  12379  oddge22np1  12387  bitsfzo  12461  gcdaddm  12500  algcvgblem  12566  cncongr1  12620  pcdvdsb  12838  pcaddlem  12857  infpnlem1  12877  prmunb  12880  imasaddfnlemg  13342  f1ghm0to0  13804  ghmf1  13805  imasring  14022  subrgdvds  14193  aprcotr  14243  quscrng  14491  metss2lem  15165  gausslemma2dlem0i  15730  gausslemma2dlem1a  15731  lgseisenlem2  15744  2sqlem6  15793  incistruhgr  15884