Theorem sylibd 149

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 144	. 2 |- ( ph -> ( ch -> th ) )
4	1, 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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3d  202  dvelimdf  2032  ceqsalt  2786  sbceqal  3041  csbiebt  3120  rspcsbela  3140  preqr1g  3792  repizf2  4191  copsexg  4273  onun2  4522  suc11g  4589  elrnrexdm  5697  isoselem  5863  riotass2  5900  oawordriexmid  6523  nnm00  6583  ecopovtrn  6686  ecopovtrng  6689  infglbti  7084  difinfsnlem  7158  enq0tr  7494  addnqprl  7589  addnqpru  7590  mulnqprl  7628  mulnqpru  7629  recexprlemss1l  7695  recexprlemss1u  7696  cauappcvgprlemdisj  7711  mulextsr1lem  7840  pitonn  7908  rereceu  7949  cnegexlem1  8194  ltadd2  8438  eqord2  8503  mulext  8633  mulgt1  8882  lt2halves  9218  addltmul  9219  nzadd  9369  ltsubnn0  9384  zextlt  9409  recnz  9410  zeo  9422  peano5uzti  9425  irradd  9711  irrmul  9712  xltneg  9902  xleadd1  9941  icc0r  9992  fznuz  10168  uznfz  10169  facndiv  10810  rennim  11146  abs00ap  11206  absle  11233  cau3lem  11258  caubnd2  11261  climshft  11447  subcn2  11454  mulcn2  11455  serf0  11495  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  efieq1re  11915  moddvds  11942  dvdsssfz1  11994  nn0seqcvgd  12179  algcvgblem  12187  eucalglt  12195  lcmgcdlem  12215  rpmul  12236  divgcdcoprm0  12239  isprm6  12285  rpexp  12291  eulerthlema  12368  eulerthlemh  12369  prmdiv  12373  pcprendvds2  12429  pcz  12470  pcprmpw  12472  pcadd2  12479  pcfac  12488  expnprm  12491  imasgrp2  13180  issubg4m  13263  znidomb  14146  tgss3  14246  cnpnei  14387  cnntr  14393  hmeoopn  14479  hmeocld  14480  mulcncflem  14761  sincosq3sgn  14963  sincosq4sgn  14964  lgsdir2lem4  15147  lgsne0  15154  2sqlem8a  15209  bj-peano4  15447  iswomni0  15541