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  2763  sbceqal  3018  csbiebt  3096  rspcsbela  3116  preqr1g  3766  repizf2  4162  copsexg  4244  onun2  4489  suc11g  4556  elrnrexdm  5655  isoselem  5820  riotass2  5856  oawordriexmid  6470  nnm00  6530  ecopovtrn  6631  ecopovtrng  6634  infglbti  7023  difinfsnlem  7097  enq0tr  7432  addnqprl  7527  addnqpru  7528  mulnqprl  7566  mulnqpru  7567  recexprlemss1l  7633  recexprlemss1u  7634  cauappcvgprlemdisj  7649  mulextsr1lem  7778  pitonn  7846  rereceu  7887  cnegexlem1  8131  ltadd2  8375  eqord2  8440  mulext  8570  mulgt1  8819  lt2halves  9153  addltmul  9154  nzadd  9304  ltsubnn0  9319  zextlt  9344  recnz  9345  zeo  9357  peano5uzti  9360  irradd  9645  irrmul  9646  xltneg  9835  xleadd1  9874  icc0r  9925  fznuz  10101  uznfz  10102  facndiv  10718  rennim  11010  abs00ap  11070  absle  11097  cau3lem  11122  caubnd2  11125  climshft  11311  subcn2  11318  mulcn2  11319  serf0  11359  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  efieq1re  11778  moddvds  11805  dvdsssfz1  11857  nn0seqcvgd  12040  algcvgblem  12048  eucalglt  12056  lcmgcdlem  12076  rpmul  12097  divgcdcoprm0  12100  isprm6  12146  rpexp  12152  eulerthlema  12229  eulerthlemh  12230  prmdiv  12234  pcprendvds2  12290  pcz  12330  pcprmpw  12332  pcfac  12347  expnprm  12350  issubg4m  13051  tgss3  13548  cnpnei  13689  cnntr  13695  hmeoopn  13781  hmeocld  13782  mulcncflem  14060  sincosq3sgn  14219  sincosq4sgn  14220  lgsdir2lem4  14402  lgsne0  14409  2sqlem8a  14439  bj-peano4  14677  iswomni0  14769