Theorem sylibd 148

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 143	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	syld 45	1 |- ( ph -> ( ps -> th ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3d  201  dvelimdf  2004  ceqsalt  2752  sbceqal  3006  csbiebt  3084  rspcsbela  3104  preqr1g  3746  repizf2  4141  copsexg  4222  onun2  4467  suc11g  4534  elrnrexdm  5624  isoselem  5788  riotass2  5824  oawordriexmid  6438  nnm00  6497  ecopovtrn  6598  ecopovtrng  6601  infglbti  6990  difinfsnlem  7064  enq0tr  7375  addnqprl  7470  addnqpru  7471  mulnqprl  7509  mulnqpru  7510  recexprlemss1l  7576  recexprlemss1u  7577  cauappcvgprlemdisj  7592  mulextsr1lem  7721  pitonn  7789  rereceu  7830  cnegexlem1  8073  ltadd2  8317  eqord2  8382  mulext  8512  mulgt1  8758  lt2halves  9092  addltmul  9093  nzadd  9243  ltsubnn0  9258  zextlt  9283  recnz  9284  zeo  9296  peano5uzti  9299  irradd  9584  irrmul  9585  xltneg  9772  xleadd1  9811  icc0r  9862  fznuz  10037  uznfz  10038  facndiv  10652  rennim  10944  abs00ap  11004  absle  11031  cau3lem  11056  caubnd2  11059  climshft  11245  subcn2  11252  mulcn2  11253  serf0  11293  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  efieq1re  11712  moddvds  11739  dvdsssfz1  11790  nn0seqcvgd  11973  algcvgblem  11981  eucalglt  11989  lcmgcdlem  12009  rpmul  12030  divgcdcoprm0  12033  isprm6  12079  rpexp  12085  eulerthlema  12162  eulerthlemh  12163  prmdiv  12167  pcprendvds2  12223  pcz  12263  pcprmpw  12265  pcfac  12280  expnprm  12283  tgss3  12718  cnpnei  12859  cnntr  12865  hmeoopn  12951  hmeocld  12952  mulcncflem  13230  sincosq3sgn  13389  sincosq4sgn  13390  lgsdir2lem4  13572  lgsne0  13579  2sqlem8a  13598  bj-peano4  13837  iswomni0  13930