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  2067  ceqsalt  2826  sbceqal  3084  csbiebt  3164  rspcsbela  3184  preqr1g  3844  repizf2  4246  copsexg  4330  onun2  4582  suc11g  4649  elrnrexdm  5776  isoselem  5950  riotass2  5989  oawordriexmid  6624  nnm00  6684  ecopovtrn  6787  ecopovtrng  6790  infglbti  7203  difinfsnlem  7277  enq0tr  7632  addnqprl  7727  addnqpru  7728  mulnqprl  7766  mulnqpru  7767  recexprlemss1l  7833  recexprlemss1u  7834  cauappcvgprlemdisj  7849  mulextsr1lem  7978  pitonn  8046  rereceu  8087  cnegexlem1  8332  ltadd2  8577  eqord2  8642  mulext  8772  mulgt1  9021  lt2halves  9358  addltmul  9359  nzadd  9510  ltsubnn0  9525  zextlt  9550  recnz  9551  zeo  9563  peano5uzti  9566  irradd  9853  irrmul  9854  xltneg  10044  xleadd1  10083  icc0r  10134  fznuz  10310  uznfz  10311  facndiv  10973  ccatalpha  11161  swrdccatin2  11276  swrdccatin2d  11291  rennim  11528  abs00ap  11588  absle  11615  cau3lem  11640  caubnd2  11643  climshft  11830  subcn2  11837  mulcn2  11838  serf0  11878  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  efieq1re  12298  moddvds  12325  dvdsssfz1  12378  nn0seqcvgd  12578  algcvgblem  12586  eucalglt  12594  lcmgcdlem  12614  rpmul  12635  divgcdcoprm0  12638  isprm6  12684  rpexp  12690  eulerthlema  12767  eulerthlemh  12768  prmdiv  12772  pcprendvds2  12829  pcz  12870  pcprmpw  12872  pcadd2  12879  pcfac  12888  expnprm  12891  imasgrp2  13662  issubg4m  13745  znidomb  14637  tgss3  14767  cnpnei  14908  cnntr  14914  hmeoopn  15000  hmeocld  15001  mulcncflem  15296  plycolemc  15447  sincosq3sgn  15517  sincosq4sgn  15518  perfect1  15687  lgsdir2lem4  15725  lgsne0  15732  lgsquad2lem2  15776  2sqlem8a  15816  bj-peano4  16373  iswomni0  16479