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  2069  ceqsalt  2829  sbceqal  3087  csbiebt  3167  rspcsbela  3187  preqr1g  3849  repizf2  4252  copsexg  4336  onun2  4588  suc11g  4655  elrnrexdm  5786  isoselem  5961  riotass2  6000  oawordriexmid  6638  nnm00  6698  ecopovtrn  6801  ecopovtrng  6804  infglbti  7224  difinfsnlem  7298  enq0tr  7654  addnqprl  7749  addnqpru  7750  mulnqprl  7788  mulnqpru  7789  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemdisj  7871  mulextsr1lem  8000  pitonn  8068  rereceu  8109  cnegexlem1  8354  ltadd2  8599  eqord2  8664  mulext  8794  mulgt1  9043  lt2halves  9380  addltmul  9381  nzadd  9532  ltsubnn0  9547  zextlt  9572  recnz  9573  zeo  9585  peano5uzti  9588  irradd  9880  irrmul  9881  xltneg  10071  xleadd1  10110  icc0r  10161  fznuz  10337  uznfz  10338  facndiv  11002  ccatalpha  11194  swrdccatin2  11314  swrdccatin2d  11329  rennim  11567  abs00ap  11627  absle  11654  cau3lem  11679  caubnd2  11682  climshft  11869  subcn2  11876  mulcn2  11877  serf0  11917  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  efieq1re  12338  moddvds  12365  dvdsssfz1  12418  nn0seqcvgd  12618  algcvgblem  12626  eucalglt  12634  lcmgcdlem  12654  rpmul  12675  divgcdcoprm0  12678  isprm6  12724  rpexp  12730  eulerthlema  12807  eulerthlemh  12808  prmdiv  12812  pcprendvds2  12869  pcz  12910  pcprmpw  12912  pcadd2  12919  pcfac  12928  expnprm  12931  imasgrp2  13702  issubg4m  13785  znidomb  14678  tgss3  14808  cnpnei  14949  cnntr  14955  hmeoopn  15041  hmeocld  15042  mulcncflem  15337  plycolemc  15488  sincosq3sgn  15558  sincosq4sgn  15559  perfect1  15728  lgsdir2lem4  15766  lgsne0  15773  lgsquad2lem2  15817  2sqlem8a  15857  clwwlkext2edg  16279  bj-peano4  16576  iswomni0  16682