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  2014  ceqsalt  2761  sbceqal  3016  csbiebt  3094  rspcsbela  3114  preqr1g  3762  repizf2  4157  copsexg  4238  onun2  4483  suc11g  4550  elrnrexdm  5647  isoselem  5811  riotass2  5847  oawordriexmid  6461  nnm00  6521  ecopovtrn  6622  ecopovtrng  6625  infglbti  7014  difinfsnlem  7088  enq0tr  7408  addnqprl  7503  addnqpru  7504  mulnqprl  7542  mulnqpru  7543  recexprlemss1l  7609  recexprlemss1u  7610  cauappcvgprlemdisj  7625  mulextsr1lem  7754  pitonn  7822  rereceu  7863  cnegexlem1  8106  ltadd2  8350  eqord2  8415  mulext  8545  mulgt1  8791  lt2halves  9125  addltmul  9126  nzadd  9276  ltsubnn0  9291  zextlt  9316  recnz  9317  zeo  9329  peano5uzti  9332  irradd  9617  irrmul  9618  xltneg  9805  xleadd1  9844  icc0r  9895  fznuz  10070  uznfz  10071  facndiv  10685  rennim  10977  abs00ap  11037  absle  11064  cau3lem  11089  caubnd2  11092  climshft  11278  subcn2  11285  mulcn2  11286  serf0  11326  cvgratnnlemnexp  11498  cvgratnnlemmn  11499  efieq1re  11745  moddvds  11772  dvdsssfz1  11823  nn0seqcvgd  12006  algcvgblem  12014  eucalglt  12022  lcmgcdlem  12042  rpmul  12063  divgcdcoprm0  12066  isprm6  12112  rpexp  12118  eulerthlema  12195  eulerthlemh  12196  prmdiv  12200  pcprendvds2  12256  pcz  12296  pcprmpw  12298  pcfac  12313  expnprm  12316  tgss3  13129  cnpnei  13270  cnntr  13276  hmeoopn  13362  hmeocld  13363  mulcncflem  13641  sincosq3sgn  13800  sincosq4sgn  13801  lgsdir2lem4  13983  lgsne0  13990  2sqlem8a  14009  bj-peano4  14247  iswomni0  14340