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  7366  difinfsnlem  7440  enq0tr  7802  addnqprl  7897  addnqpru  7898  mulnqprl  7936  mulnqpru  7937  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemdisj  8019  mulextsr1lem  8148  pitonn  8216  rereceu  8257  cnegexlem1  8503  ltadd2  8749  eqord2  8814  mulext  8945  mulgt1  9196  lt2halves  9546  addltmul  9547  nzadd  9702  ltsubnn0  9717  zextlt  9743  recnz  9744  zeo  9756  peano5uzti  9759  irradd  10056  irrmul  10058  xltneg  10249  xleadd1  10288  icc0r  10339  fznuz  10520  uznfz  10521  facndiv  11193  hashf1  11303  ccatalpha  11397  swrdccatin2  11517  swrdccatin2d  11532  rennim  11784  abs00ap  11844  absle  11872  cau3lem  11897  caubnd2  11900  climshft  12089  subcn2  12096  mulcn2  12097  serf0  12137  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  efieq1re  12558  moddvds  12585  dvdsssfz1  12638  nn0seqcvgd  12838  algcvgblem  12846  eucalglt  12854  lcmgcdlem  12874  rpmul  12895  divgcdcoprm0  12898  isprm6  12945  rpexp  12951  eulerthlema  13031  eulerthlemh  13032  prmdiv  13036  pcprendvds2  13093  pcz  13134  pcprmpw  13136  pcadd2  13143  pcfac  13152  expnprm  13155  imasgrp2  13966  issubg4m  14049  znidomb  15077  tgss3  15270  cnpnei  15411  cnntr  15417  hmeoopn  15503  hmeocld  15504  mulcncflem  15799  plycolemc  15950  sincosq3sgn  16021  sincosq4sgn  16022  chtqub  16257  perfect1  16259  lgsdir2lem4  16316  lgsne0  16323  lgsquad2lem2  16367  2sqlem8a  16407  clwwlkext2edg  16829  bj-peano4  17147  iswomni0  17268