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  2072  ceqsalt  2842  sbceqal  3101  csbiebt  3181  rspcsbela  3201  preqr1g  3875  repizf2  4280  copsexg  4365  onun2  4617  suc11g  4684  elrnrexdm  5821  isoselem  5999  riotass2  6040  oawordriexmid  6716  nnm00  6776  ecopovtrn  6879  ecopovtrng  6882  infglbti  7329  difinfsnlem  7403  enq0tr  7765  addnqprl  7860  addnqpru  7861  mulnqprl  7899  mulnqpru  7900  recexprlemss1l  7966  recexprlemss1u  7967  cauappcvgprlemdisj  7982  mulextsr1lem  8111  pitonn  8179  rereceu  8220  cnegexlem1  8464  ltadd2  8710  eqord2  8775  mulext  8905  mulgt1  9154  lt2halves  9491  addltmul  9492  nzadd  9647  ltsubnn0  9662  zextlt  9688  recnz  9689  zeo  9701  peano5uzti  9704  irradd  9996  irrmul  9997  xltneg  10188  xleadd1  10227  icc0r  10278  fznuz  10458  uznfz  10459  facndiv  11126  ccatalpha  11326  swrdccatin2  11446  swrdccatin2d  11461  rennim  11712  abs00ap  11772  absle  11799  cau3lem  11824  caubnd2  11827  climshft  12014  subcn2  12021  mulcn2  12022  serf0  12062  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  efieq1re  12483  moddvds  12510  dvdsssfz1  12563  nn0seqcvgd  12763  algcvgblem  12771  eucalglt  12779  lcmgcdlem  12799  rpmul  12820  divgcdcoprm0  12823  isprm6  12869  rpexp  12875  eulerthlema  12952  eulerthlemh  12953  prmdiv  12957  pcprendvds2  13014  pcz  13055  pcprmpw  13057  pcadd2  13064  pcfac  13073  expnprm  13076  imasgrp2  13863  issubg4m  13946  znidomb  14932  tgss3  15069  cnpnei  15210  cnntr  15216  hmeoopn  15302  hmeocld  15303  mulcncflem  15598  plycolemc  15749  sincosq3sgn  15819  sincosq4sgn  15820  perfect1  15992  lgsdir2lem4  16030  lgsne0  16037  lgsquad2lem2  16081  2sqlem8a  16121  clwwlkext2edg  16543  bj-peano4  16851  iswomni0  16962