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  4299  copsexg  4384  onun2  4637  suc11g  4704  elrnrexdm  5847  isoselem  6026  riotass2  6067  oawordriexmid  6743  nnm00  6803  ecopovtrn  6906  ecopovtrng  6909  infglbti  7365  difinfsnlem  7439  enq0tr  7801  addnqprl  7896  addnqpru  7897  mulnqprl  7935  mulnqpru  7936  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemdisj  8018  mulextsr1lem  8147  pitonn  8215  rereceu  8256  cnegexlem1  8501  ltadd2  8747  eqord2  8812  mulext  8942  mulgt1  9193  lt2halves  9541  addltmul  9542  nzadd  9697  ltsubnn0  9712  zextlt  9738  recnz  9739  zeo  9751  peano5uzti  9754  irradd  10046  irrmul  10047  xltneg  10238  xleadd1  10277  icc0r  10328  fznuz  10509  uznfz  10510  facndiv  11177  hashf1  11287  ccatalpha  11381  swrdccatin2  11501  swrdccatin2d  11516  rennim  11768  abs00ap  11828  absle  11855  cau3lem  11880  caubnd2  11883  climshft  12070  subcn2  12077  mulcn2  12078  serf0  12118  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  efieq1re  12539  moddvds  12566  dvdsssfz1  12619  nn0seqcvgd  12819  algcvgblem  12827  eucalglt  12835  lcmgcdlem  12855  rpmul  12876  divgcdcoprm0  12879  isprm6  12925  rpexp  12931  eulerthlema  13008  eulerthlemh  13009  prmdiv  13013  pcprendvds2  13070  pcz  13111  pcprmpw  13113  pcadd2  13120  pcfac  13129  expnprm  13132  imasgrp2  13913  issubg4m  13996  znidomb  14993  tgss3  15179  cnpnei  15320  cnntr  15326  hmeoopn  15412  hmeocld  15413  mulcncflem  15708  plycolemc  15859  sincosq3sgn  15929  sincosq4sgn  15930  perfect1  16112  lgsdir2lem4  16150  lgsne0  16157  lgsquad2lem2  16201  2sqlem8a  16241  clwwlkext2edg  16663  bj-peano4  16981  iswomni0  17101