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  2043  ceqsalt  2797  sbceqal  3053  csbiebt  3132  rspcsbela  3152  preqr1g  3806  repizf2  4205  copsexg  4287  onun2  4537  suc11g  4604  elrnrexdm  5718  isoselem  5888  riotass2  5925  oawordriexmid  6555  nnm00  6615  ecopovtrn  6718  ecopovtrng  6721  infglbti  7126  difinfsnlem  7200  enq0tr  7546  addnqprl  7641  addnqpru  7642  mulnqprl  7680  mulnqpru  7681  recexprlemss1l  7747  recexprlemss1u  7748  cauappcvgprlemdisj  7763  mulextsr1lem  7892  pitonn  7960  rereceu  8001  cnegexlem1  8246  ltadd2  8491  eqord2  8556  mulext  8686  mulgt1  8935  lt2halves  9272  addltmul  9273  nzadd  9424  ltsubnn0  9439  zextlt  9464  recnz  9465  zeo  9477  peano5uzti  9480  irradd  9766  irrmul  9767  xltneg  9957  xleadd1  9996  icc0r  10047  fznuz  10223  uznfz  10224  facndiv  10882  rennim  11284  abs00ap  11344  absle  11371  cau3lem  11396  caubnd2  11399  climshft  11586  subcn2  11593  mulcn2  11594  serf0  11634  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  efieq1re  12054  moddvds  12081  dvdsssfz1  12134  nn0seqcvgd  12334  algcvgblem  12342  eucalglt  12350  lcmgcdlem  12370  rpmul  12391  divgcdcoprm0  12394  isprm6  12440  rpexp  12446  eulerthlema  12523  eulerthlemh  12524  prmdiv  12528  pcprendvds2  12585  pcz  12626  pcprmpw  12628  pcadd2  12635  pcfac  12644  expnprm  12647  imasgrp2  13417  issubg4m  13500  znidomb  14391  tgss3  14521  cnpnei  14662  cnntr  14668  hmeoopn  14754  hmeocld  14755  mulcncflem  15050  plycolemc  15201  sincosq3sgn  15271  sincosq4sgn  15272  perfect1  15441  lgsdir2lem4  15479  lgsne0  15486  lgsquad2lem2  15530  2sqlem8a  15570  bj-peano4  15853  iswomni0  15952