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-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3d  201  dvelimdf  2009  ceqsalt  2756  sbceqal  3010  csbiebt  3088  rspcsbela  3108  preqr1g  3753  repizf2  4148  copsexg  4229  onun2  4474  suc11g  4541  elrnrexdm  5635  isoselem  5799  riotass2  5835  oawordriexmid  6449  nnm00  6509  ecopovtrn  6610  ecopovtrng  6613  infglbti  7002  difinfsnlem  7076  enq0tr  7396  addnqprl  7491  addnqpru  7492  mulnqprl  7530  mulnqpru  7531  recexprlemss1l  7597  recexprlemss1u  7598  cauappcvgprlemdisj  7613  mulextsr1lem  7742  pitonn  7810  rereceu  7851  cnegexlem1  8094  ltadd2  8338  eqord2  8403  mulext  8533  mulgt1  8779  lt2halves  9113  addltmul  9114  nzadd  9264  ltsubnn0  9279  zextlt  9304  recnz  9305  zeo  9317  peano5uzti  9320  irradd  9605  irrmul  9606  xltneg  9793  xleadd1  9832  icc0r  9883  fznuz  10058  uznfz  10059  facndiv  10673  rennim  10966  abs00ap  11026  absle  11053  cau3lem  11078  caubnd2  11081  climshft  11267  subcn2  11274  mulcn2  11275  serf0  11315  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  efieq1re  11734  moddvds  11761  dvdsssfz1  11812  nn0seqcvgd  11995  algcvgblem  12003  eucalglt  12011  lcmgcdlem  12031  rpmul  12052  divgcdcoprm0  12055  isprm6  12101  rpexp  12107  eulerthlema  12184  eulerthlemh  12185  prmdiv  12189  pcprendvds2  12245  pcz  12285  pcprmpw  12287  pcfac  12302  expnprm  12305  tgss3  12872  cnpnei  13013  cnntr  13019  hmeoopn  13105  hmeocld  13106  mulcncflem  13384  sincosq3sgn  13543  sincosq4sgn  13544  lgsdir2lem4  13726  lgsne0  13733  2sqlem8a  13752  bj-peano4  13990  iswomni0  14083