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  2827  sbceqal  3085  csbiebt  3165  rspcsbela  3185  preqr1g  3847  repizf2  4250  copsexg  4334  onun2  4586  suc11g  4653  elrnrexdm  5782  isoselem  5956  riotass2  5995  oawordriexmid  6633  nnm00  6693  ecopovtrn  6796  ecopovtrng  6799  infglbti  7215  difinfsnlem  7289  enq0tr  7644  addnqprl  7739  addnqpru  7740  mulnqprl  7778  mulnqpru  7779  recexprlemss1l  7845  recexprlemss1u  7846  cauappcvgprlemdisj  7861  mulextsr1lem  7990  pitonn  8058  rereceu  8099  cnegexlem1  8344  ltadd2  8589  eqord2  8654  mulext  8784  mulgt1  9033  lt2halves  9370  addltmul  9371  nzadd  9522  ltsubnn0  9537  zextlt  9562  recnz  9563  zeo  9575  peano5uzti  9578  irradd  9870  irrmul  9871  xltneg  10061  xleadd1  10100  icc0r  10151  fznuz  10327  uznfz  10328  facndiv  10991  ccatalpha  11180  swrdccatin2  11300  swrdccatin2d  11315  rennim  11553  abs00ap  11613  absle  11640  cau3lem  11665  caubnd2  11668  climshft  11855  subcn2  11862  mulcn2  11863  serf0  11903  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  efieq1re  12323  moddvds  12350  dvdsssfz1  12403  nn0seqcvgd  12603  algcvgblem  12611  eucalglt  12619  lcmgcdlem  12639  rpmul  12660  divgcdcoprm0  12663  isprm6  12709  rpexp  12715  eulerthlema  12792  eulerthlemh  12793  prmdiv  12797  pcprendvds2  12854  pcz  12895  pcprmpw  12897  pcadd2  12904  pcfac  12913  expnprm  12916  imasgrp2  13687  issubg4m  13770  znidomb  14662  tgss3  14792  cnpnei  14933  cnntr  14939  hmeoopn  15025  hmeocld  15026  mulcncflem  15321  plycolemc  15472  sincosq3sgn  15542  sincosq4sgn  15543  perfect1  15712  lgsdir2lem4  15750  lgsne0  15757  lgsquad2lem2  15801  2sqlem8a  15841  clwwlkext2edg  16217  bj-peano4  16486  iswomni0  16591