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  6748  nnm00  6808  ecopovtrn  6911  ecopovtrng  6914  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  9706  ltsubnn0  9721  zextlt  9748  recnz  9749  zeo  9761  peano5uzti  9764  irradd  10061  irrmul  10063  xltneg  10254  xleadd1  10293  icc0r  10344  fznuz  10525  uznfz  10526  facndiv  11198  hashf1  11308  ccatalpha  11402  swrdccatin2  11522  swrdccatin2d  11537  rennim  11789  abs00ap  11849  absle  11877  cau3lem  11902  caubnd2  11905  climshft  12094  subcn2  12101  mulcn2  12102  serf0  12142  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  efieq1re  12563  moddvds  12590  dvdsssfz1  12643  nn0seqcvgd  12843  algcvgblem  12851  eucalglt  12859  lcmgcdlem  12879  rpmul  12900  divgcdcoprm0  12903  isprm6  12950  rpexp  12956  eulerthlema  13036  eulerthlemh  13037  prmdiv  13041  pcprendvds2  13098  pcz  13139  pcprmpw  13141  pcadd2  13148  pcfac  13157  expnprm  13160  imasgrp2  13971  issubg4m  14054  znidomb  15101  tgss3  15321  cnpnei  15462  cnntr  15468  hmeoopn  15554  hmeocld  15555  mulcncflem  15850  plycolemc  16001  sincosq3sgn  16072  sincosq4sgn  16073  sineq0re  16093  chtqub  16313  perfect1  16315  lgsdir2lem4  16372  lgsne0  16379  lgsquad2lem2  16423  2sqlem8a  16463  clwwlkext2edg  16885  bj-peano4  17203  iswomni0  17325