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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3d  202  dvelimdf  2067  ceqsalt  2826  sbceqal  3084  csbiebt  3164  rspcsbela  3184  preqr1g  3843  repizf2  4245  copsexg  4329  onun2  4581  suc11g  4648  elrnrexdm  5773  isoselem  5943  riotass2  5982  oawordriexmid  6614  nnm00  6674  ecopovtrn  6777  ecopovtrng  6780  infglbti  7188  difinfsnlem  7262  enq0tr  7617  addnqprl  7712  addnqpru  7713  mulnqprl  7751  mulnqpru  7752  recexprlemss1l  7818  recexprlemss1u  7819  cauappcvgprlemdisj  7834  mulextsr1lem  7963  pitonn  8031  rereceu  8072  cnegexlem1  8317  ltadd2  8562  eqord2  8627  mulext  8757  mulgt1  9006  lt2halves  9343  addltmul  9344  nzadd  9495  ltsubnn0  9510  zextlt  9535  recnz  9536  zeo  9548  peano5uzti  9551  irradd  9837  irrmul  9838  xltneg  10028  xleadd1  10067  icc0r  10118  fznuz  10294  uznfz  10295  facndiv  10956  swrdccatin2  11256  swrdccatin2d  11271  rennim  11508  abs00ap  11568  absle  11595  cau3lem  11620  caubnd2  11623  climshft  11810  subcn2  11817  mulcn2  11818  serf0  11858  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  efieq1re  12278  moddvds  12305  dvdsssfz1  12358  nn0seqcvgd  12558  algcvgblem  12566  eucalglt  12574  lcmgcdlem  12594  rpmul  12615  divgcdcoprm0  12618  isprm6  12664  rpexp  12670  eulerthlema  12747  eulerthlemh  12748  prmdiv  12752  pcprendvds2  12809  pcz  12850  pcprmpw  12852  pcadd2  12859  pcfac  12868  expnprm  12871  imasgrp2  13642  issubg4m  13725  znidomb  14616  tgss3  14746  cnpnei  14887  cnntr  14893  hmeoopn  14979  hmeocld  14980  mulcncflem  15275  plycolemc  15426  sincosq3sgn  15496  sincosq4sgn  15497  perfect1  15666  lgsdir2lem4  15704  lgsne0  15711  lgsquad2lem2  15755  2sqlem8a  15795  bj-peano4  16276  iswomni0  16378