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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3d  202  dvelimdf  2076  ceqsalt  2848  sbceqal  3107  csbiebt  3187  rspcsbela  3207  preqr1g  3891  repizf2  4301  copsexg  4386  onun2  4639  suc11g  4706  elrnrexdm  5850  isoselem  6029  riotass2  6070  oawordriexmid  6747  nnm00  6807  ecopovtrn  6910  ecopovtrng  6913  infglbti  7371  difinfsnlem  7445  enq0tr  7807  addnqprl  7902  addnqpru  7903  mulnqprl  7941  mulnqpru  7942  recexprlemss1l  8008  recexprlemss1u  8009  cauappcvgprlemdisj  8024  mulextsr1lem  8153  pitonn  8221  rereceu  8262  cnegexlem1  8508  ltadd2  8754  eqord2  8819  mulext  8950  mulgt1  9201  lt2halves  9552  addltmul  9553  nzadd  9708  ltsubnn0  9723  zextlt  9749  recnz  9750  zeo  9762  peano5uzti  9765  irradd  10062  irrmul  10064  xltneg  10255  xleadd1  10294  icc0r  10345  fznuz  10526  uznfz  10527  facndiv  11199  hashf1  11309  ccatalpha  11403  swrdccatin2  11523  swrdccatin2d  11538  rennim  11790  abs00ap  11850  absle  11878  cau3lem  11903  caubnd2  11906  climshft  12095  subcn2  12102  mulcn2  12103  serf0  12143  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  efieq1re  12564  moddvds  12591  dvdsssfz1  12644  nn0seqcvgd  12844  algcvgblem  12852  eucalglt  12860  lcmgcdlem  12880  rpmul  12901  divgcdcoprm0  12904  isprm6  12951  rpexp  12957  eulerthlema  13037  eulerthlemh  13038  prmdiv  13042  pcprendvds2  13099  pcz  13140  pcprmpw  13142  pcadd2  13149  pcfac  13158  expnprm  13161  imasgrp2  13972  issubg4m  14055  znidomb  15102  tgss3  15304  cnpnei  15445  cnntr  15451  hmeoopn  15537  hmeocld  15538  mulcncflem  15833  plycolemc  15984  sincosq3sgn  16055  sincosq4sgn  16056  sineq0re  16076  chtqub  16296  perfect1  16298  lgsdir2lem4  16355  lgsne0  16362  lgsquad2lem2  16406  2sqlem8a  16446  clwwlkext2edg  16868  bj-peano4  17186  iswomni0  17308