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  2045  ceqsalt  2800  sbceqal  3058  csbiebt  3137  rspcsbela  3157  preqr1g  3813  repizf2  4214  copsexg  4296  onun2  4546  suc11g  4613  elrnrexdm  5732  isoselem  5902  riotass2  5939  oawordriexmid  6569  nnm00  6629  ecopovtrn  6732  ecopovtrng  6735  infglbti  7142  difinfsnlem  7216  enq0tr  7567  addnqprl  7662  addnqpru  7663  mulnqprl  7701  mulnqpru  7702  recexprlemss1l  7768  recexprlemss1u  7769  cauappcvgprlemdisj  7784  mulextsr1lem  7913  pitonn  7981  rereceu  8022  cnegexlem1  8267  ltadd2  8512  eqord2  8577  mulext  8707  mulgt1  8956  lt2halves  9293  addltmul  9294  nzadd  9445  ltsubnn0  9460  zextlt  9485  recnz  9486  zeo  9498  peano5uzti  9501  irradd  9787  irrmul  9788  xltneg  9978  xleadd1  10017  icc0r  10068  fznuz  10244  uznfz  10245  facndiv  10906  rennim  11388  abs00ap  11448  absle  11475  cau3lem  11500  caubnd2  11503  climshft  11690  subcn2  11697  mulcn2  11698  serf0  11738  cvgratnnlemnexp  11910  cvgratnnlemmn  11911  efieq1re  12158  moddvds  12185  dvdsssfz1  12238  nn0seqcvgd  12438  algcvgblem  12446  eucalglt  12454  lcmgcdlem  12474  rpmul  12495  divgcdcoprm0  12498  isprm6  12544  rpexp  12550  eulerthlema  12627  eulerthlemh  12628  prmdiv  12632  pcprendvds2  12689  pcz  12730  pcprmpw  12732  pcadd2  12739  pcfac  12748  expnprm  12751  imasgrp2  13521  issubg4m  13604  znidomb  14495  tgss3  14625  cnpnei  14766  cnntr  14772  hmeoopn  14858  hmeocld  14859  mulcncflem  15154  plycolemc  15305  sincosq3sgn  15375  sincosq4sgn  15376  perfect1  15545  lgsdir2lem4  15583  lgsne0  15590  lgsquad2lem2  15634  2sqlem8a  15674  bj-peano4  16029  iswomni0  16131