Theorem sylibd 147

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 142	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	syld 44	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr3d  200  dvelimdf  1934  ceqsalt  2626  sbceqal  2870  csbiebt  2943  rspcsbela  2962  preqr1g  3566  repizf2  3944  copsexg  4007  onun2  4242  suc11g  4308  elrnrexdm  5338  isoselem  5490  riotass2  5525  oawordriexmid  6114  nnm00  6168  ecopovtrn  6269  ecopovtrng  6272  infglbti  6497  enq0tr  6686  addnqprl  6781  addnqpru  6782  mulnqprl  6820  mulnqpru  6821  recexprlemss1l  6887  recexprlemss1u  6888  cauappcvgprlemdisj  6903  mulextsr1lem  7018  pitonn  7078  rereceu  7117  cnegexlem1  7350  ltadd2  7590  mulext  7781  mulgt1  8008  lt2halves  8333  addltmul  8334  nzadd  8484  zextlt  8520  recnz  8521  zeo  8533  peano5uzti  8536  irradd  8812  irrmul  8813  xltneg  8979  icc0r  9025  fznuz  9195  uznfz  9196  facndiv  9763  rennim  10026  abs00ap  10086  absle  10113  cau3lem  10138  caubnd2  10141  climshft  10281  subcn2  10288  mulcn2  10289  serif0  10327  moddvds  10349  dvdsssfz1  10397  nn0seqcvgd  10567  algcvgblem  10575  eucalglt  10583  lcmgcdlem  10603  rpmul  10624  divgcdcoprm0  10627  isprm6  10670  rpexp  10676  bj-peano4  10908