Theorem sylibd 147

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylibd.1	|- ( ph -> ( ps -> ch ) )
sylibd.2	|- ( ph -> ( ch <-> th ) )

Assertion

Ref	Expression
sylibd	|- ( ph -> ( ps -> th ) )

Proof of Theorem sylibd

Step	Hyp	Ref	Expression
1		sylibd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		sylibd.2	. . 3 |- ( ph -> ( ch <-> th ) )
3	2	biimpd 142	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	syld 44	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr3d  200  dvelimdf  1933  ceqsalt  2625  sbceqal  2869  csbiebt  2942  rspcsbela  2961  preqr1g  3558  repizf2  3936  copsexg  3999  onun2  4234  suc11g  4300  elrnrexdm  5327  isoselem  5479  riotass2  5514  nnm00  6125  ecopovtrn  6226  ecopovtrng  6229  infglbti  6438  enq0tr  6624  addnqprl  6719  addnqpru  6720  mulnqprl  6758  mulnqpru  6759  recexprlemss1l  6825  recexprlemss1u  6826  cauappcvgprlemdisj  6841  mulextsr1lem  6956  pitonn  7016  rereceu  7055  cnegexlem1  7283  ltadd2  7523  mulext  7714  mulgt1  7941  lt2halves  8266  addltmul  8267  nzadd  8403  zextlt  8439  recnz  8440  zeo  8452  peano5uzti  8455  irradd  8731  irrmul  8732  xltneg  8903  icc0r  8949  fznuz  9119  uznfz  9120  facndiv  9666  rennim  9888  abs00ap  9948  absle  9975  cau3lem  10000  caubnd2  10003  climshft  10143  subcn2  10150  mulcn2  10151  serif0  10189  moddvds  10204  dvdsssfz1  10252  nn0seqcvgd  10423  algcvgblem  10431  eucalglt  10439  lcmgcdlem  10459  rpmul  10480  divgcdcoprm0  10483  isprm6  10526  rpexp  10532  bj-peano4  10750