Theorem sylibd 148

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3d  201  dvelimdf  1952  ceqsalt  2667  sbceqal  2916  csbiebt  2989  rspcsbela  3009  preqr1g  3640  repizf2  4026  copsexg  4104  onun2  4344  suc11g  4410  elrnrexdm  5491  isoselem  5653  riotass2  5688  oawordriexmid  6296  nnm00  6355  ecopovtrn  6456  ecopovtrng  6459  infglbti  6827  difinfsnlem  6899  enq0tr  7143  addnqprl  7238  addnqpru  7239  mulnqprl  7277  mulnqpru  7278  recexprlemss1l  7344  recexprlemss1u  7345  cauappcvgprlemdisj  7360  mulextsr1lem  7475  pitonn  7535  rereceu  7574  cnegexlem1  7808  ltadd2  8048  eqord2  8113  mulext  8242  mulgt1  8479  lt2halves  8807  addltmul  8808  nzadd  8958  zextlt  8995  recnz  8996  zeo  9008  peano5uzti  9011  irradd  9288  irrmul  9289  xltneg  9460  xleadd1  9499  icc0r  9550  fznuz  9723  uznfz  9724  facndiv  10326  rennim  10614  abs00ap  10674  absle  10701  cau3lem  10726  caubnd2  10729  climshft  10912  subcn2  10919  mulcn2  10920  serf0  10960  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  efieq1re  11275  moddvds  11297  dvdsssfz1  11345  nn0seqcvgd  11515  algcvgblem  11523  eucalglt  11531  lcmgcdlem  11551  rpmul  11572  divgcdcoprm0  11575  isprm6  11618  rpexp  11624  tgss3  12029  cnpnei  12169  cnntr  12175  mulcncflem  12502  bj-peano4  12738