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  5960  riotass2  5999  oawordriexmid  6637  nnm00  6697  ecopovtrn  6800  ecopovtrng  6803  infglbti  7223  difinfsnlem  7297  enq0tr  7653  addnqprl  7748  addnqpru  7749  mulnqprl  7787  mulnqpru  7788  recexprlemss1l  7854  recexprlemss1u  7855  cauappcvgprlemdisj  7870  mulextsr1lem  7999  pitonn  8067  rereceu  8108  cnegexlem1  8353  ltadd2  8598  eqord2  8663  mulext  8793  mulgt1  9042  lt2halves  9379  addltmul  9380  nzadd  9531  ltsubnn0  9546  zextlt  9571  recnz  9572  zeo  9584  peano5uzti  9587  irradd  9879  irrmul  9880  xltneg  10070  xleadd1  10109  icc0r  10160  fznuz  10336  uznfz  10337  facndiv  11000  ccatalpha  11189  swrdccatin2  11309  swrdccatin2d  11324  rennim  11562  abs00ap  11622  absle  11649  cau3lem  11674  caubnd2  11677  climshft  11864  subcn2  11871  mulcn2  11872  serf0  11912  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  efieq1re  12332  moddvds  12359  dvdsssfz1  12412  nn0seqcvgd  12612  algcvgblem  12620  eucalglt  12628  lcmgcdlem  12648  rpmul  12669  divgcdcoprm0  12672  isprm6  12718  rpexp  12724  eulerthlema  12801  eulerthlemh  12802  prmdiv  12806  pcprendvds2  12863  pcz  12904  pcprmpw  12906  pcadd2  12913  pcfac  12922  expnprm  12925  imasgrp2  13696  issubg4m  13779  znidomb  14671  tgss3  14801  cnpnei  14942  cnntr  14948  hmeoopn  15034  hmeocld  15035  mulcncflem  15330  plycolemc  15481  sincosq3sgn  15551  sincosq4sgn  15552  perfect1  15721  lgsdir2lem4  15759  lgsne0  15766  lgsquad2lem2  15810  2sqlem8a  15850  clwwlkext2edg  16272  bj-peano4  16550  iswomni0  16655