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  11255  abs00ap  11315  absle  11342  cau3lem  11367  caubnd2  11370  climshft  11557  subcn2  11564  mulcn2  11565  serf0  11605  cvgratnnlemnexp  11777  cvgratnnlemmn  11778  efieq1re  12025  moddvds  12052  dvdsssfz1  12105  nn0seqcvgd  12305  algcvgblem  12313  eucalglt  12321  lcmgcdlem  12341  rpmul  12362  divgcdcoprm0  12365  isprm6  12411  rpexp  12417  eulerthlema  12494  eulerthlemh  12495  prmdiv  12499  pcprendvds2  12556  pcz  12597  pcprmpw  12599  pcadd2  12606  pcfac  12615  expnprm  12618  imasgrp2  13388  issubg4m  13471  znidomb  14362  tgss3  14492  cnpnei  14633  cnntr  14639  hmeoopn  14725  hmeocld  14726  mulcncflem  15021  plycolemc  15172  sincosq3sgn  15242  sincosq4sgn  15243  perfect1  15412  lgsdir2lem4  15450  lgsne0  15457  lgsquad2lem2  15501  2sqlem8a  15541  bj-peano4  15824  iswomni0  15923