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  2069  ceqsalt  2830  sbceqal  3088  csbiebt  3168  rspcsbela  3188  preqr1g  3854  repizf2  4258  copsexg  4342  onun2  4594  suc11g  4661  elrnrexdm  5794  isoselem  5971  riotass2  6010  oawordriexmid  6681  nnm00  6741  ecopovtrn  6844  ecopovtrng  6847  infglbti  7267  difinfsnlem  7341  enq0tr  7697  addnqprl  7792  addnqpru  7793  mulnqprl  7831  mulnqpru  7832  recexprlemss1l  7898  recexprlemss1u  7899  cauappcvgprlemdisj  7914  mulextsr1lem  8043  pitonn  8111  rereceu  8152  cnegexlem1  8396  ltadd2  8641  eqord2  8706  mulext  8836  mulgt1  9085  lt2halves  9422  addltmul  9423  nzadd  9576  ltsubnn0  9591  zextlt  9616  recnz  9617  zeo  9629  peano5uzti  9632  irradd  9924  irrmul  9925  xltneg  10115  xleadd1  10154  icc0r  10205  fznuz  10382  uznfz  10383  facndiv  11047  ccatalpha  11239  swrdccatin2  11359  swrdccatin2d  11374  rennim  11625  abs00ap  11685  absle  11712  cau3lem  11737  caubnd2  11740  climshft  11927  subcn2  11934  mulcn2  11935  serf0  11975  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  efieq1re  12396  moddvds  12423  dvdsssfz1  12476  nn0seqcvgd  12676  algcvgblem  12684  eucalglt  12692  lcmgcdlem  12712  rpmul  12733  divgcdcoprm0  12736  isprm6  12782  rpexp  12788  eulerthlema  12865  eulerthlemh  12866  prmdiv  12870  pcprendvds2  12927  pcz  12968  pcprmpw  12970  pcadd2  12977  pcfac  12986  expnprm  12989  imasgrp2  13760  issubg4m  13843  znidomb  14737  tgss3  14872  cnpnei  15013  cnntr  15019  hmeoopn  15105  hmeocld  15106  mulcncflem  15401  plycolemc  15552  sincosq3sgn  15622  sincosq4sgn  15623  perfect1  15795  lgsdir2lem4  15833  lgsne0  15840  lgsquad2lem2  15884  2sqlem8a  15924  clwwlkext2edg  16346  bj-peano4  16654  iswomni0  16767