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  2070  ceqsalt  2840  sbceqal  3098  csbiebt  3178  rspcsbela  3198  preqr1g  3870  repizf2  4275  copsexg  4360  onun2  4612  suc11g  4679  elrnrexdm  5816  isoselem  5993  riotass2  6032  oawordriexmid  6703  nnm00  6763  ecopovtrn  6866  ecopovtrng  6869  infglbti  7316  difinfsnlem  7390  enq0tr  7749  addnqprl  7844  addnqpru  7845  mulnqprl  7883  mulnqpru  7884  recexprlemss1l  7950  recexprlemss1u  7951  cauappcvgprlemdisj  7966  mulextsr1lem  8095  pitonn  8163  rereceu  8204  cnegexlem1  8448  ltadd2  8693  eqord2  8758  mulext  8888  mulgt1  9137  lt2halves  9474  addltmul  9475  nzadd  9630  ltsubnn0  9645  zextlt  9670  recnz  9671  zeo  9683  peano5uzti  9686  irradd  9978  irrmul  9979  xltneg  10169  xleadd1  10208  icc0r  10259  fznuz  10436  uznfz  10437  facndiv  11101  ccatalpha  11301  swrdccatin2  11421  swrdccatin2d  11436  rennim  11687  abs00ap  11747  absle  11774  cau3lem  11799  caubnd2  11802  climshft  11989  subcn2  11996  mulcn2  11997  serf0  12037  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  efieq1re  12458  moddvds  12485  dvdsssfz1  12538  nn0seqcvgd  12738  algcvgblem  12746  eucalglt  12754  lcmgcdlem  12774  rpmul  12795  divgcdcoprm0  12798  isprm6  12844  rpexp  12850  eulerthlema  12927  eulerthlemh  12928  prmdiv  12932  pcprendvds2  12989  pcz  13030  pcprmpw  13032  pcadd2  13039  pcfac  13048  expnprm  13051  imasgrp2  13827  issubg4m  13910  znidomb  14806  tgss3  14943  cnpnei  15084  cnntr  15090  hmeoopn  15176  hmeocld  15177  mulcncflem  15472  plycolemc  15623  sincosq3sgn  15693  sincosq4sgn  15694  perfect1  15866  lgsdir2lem4  15904  lgsne0  15911  lgsquad2lem2  15955  2sqlem8a  15995  clwwlkext2edg  16417  bj-peano4  16725  iswomni0  16836