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  2016  ceqsalt  2764  sbceqal  3019  csbiebt  3097  rspcsbela  3117  preqr1g  3767  repizf2  4163  copsexg  4245  onun2  4490  suc11g  4557  elrnrexdm  5656  isoselem  5821  riotass2  5857  oawordriexmid  6471  nnm00  6531  ecopovtrn  6632  ecopovtrng  6635  infglbti  7024  difinfsnlem  7098  enq0tr  7433  addnqprl  7528  addnqpru  7529  mulnqprl  7567  mulnqpru  7568  recexprlemss1l  7634  recexprlemss1u  7635  cauappcvgprlemdisj  7650  mulextsr1lem  7779  pitonn  7847  rereceu  7888  cnegexlem1  8132  ltadd2  8376  eqord2  8441  mulext  8571  mulgt1  8820  lt2halves  9154  addltmul  9155  nzadd  9305  ltsubnn0  9320  zextlt  9345  recnz  9346  zeo  9358  peano5uzti  9361  irradd  9646  irrmul  9647  xltneg  9836  xleadd1  9875  icc0r  9926  fznuz  10102  uznfz  10103  facndiv  10719  rennim  11011  abs00ap  11071  absle  11098  cau3lem  11123  caubnd2  11126  climshft  11312  subcn2  11319  mulcn2  11320  serf0  11360  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  efieq1re  11779  moddvds  11806  dvdsssfz1  11858  nn0seqcvgd  12041  algcvgblem  12049  eucalglt  12057  lcmgcdlem  12077  rpmul  12098  divgcdcoprm0  12101  isprm6  12147  rpexp  12153  eulerthlema  12230  eulerthlemh  12231  prmdiv  12235  pcprendvds2  12291  pcz  12331  pcprmpw  12333  pcfac  12348  expnprm  12351  issubg4m  13053  tgss3  13581  cnpnei  13722  cnntr  13728  hmeoopn  13814  hmeocld  13815  mulcncflem  14093  sincosq3sgn  14252  sincosq4sgn  14253  lgsdir2lem4  14435  lgsne0  14442  2sqlem8a  14472  bj-peano4  14710  iswomni0  14802