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  8502  ltadd2  8748  eqord2  8813  mulext  8944  mulgt1  9195  lt2halves  9545  addltmul  9546  nzadd  9701  ltsubnn0  9716  zextlt  9742  recnz  9743  zeo  9755  peano5uzti  9758  irradd  10055  irrmul  10057  xltneg  10248  xleadd1  10287  icc0r  10338  fznuz  10519  uznfz  10520  facndiv  11191  hashf1  11301  ccatalpha  11395  swrdccatin2  11515  swrdccatin2d  11530  rennim  11782  abs00ap  11842  absle  11870  cau3lem  11895  caubnd2  11898  climshft  12086  subcn2  12093  mulcn2  12094  serf0  12134  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  efieq1re  12555  moddvds  12582  dvdsssfz1  12635  nn0seqcvgd  12835  algcvgblem  12843  eucalglt  12851  lcmgcdlem  12871  rpmul  12892  divgcdcoprm0  12895  isprm6  12942  rpexp  12948  eulerthlema  13028  eulerthlemh  13029  prmdiv  13033  pcprendvds2  13090  pcz  13131  pcprmpw  13133  pcadd2  13140  pcfac  13149  expnprm  13152  imasgrp2  13962  issubg4m  14045  znidomb  15042  tgss3  15228  cnpnei  15369  cnntr  15375  hmeoopn  15461  hmeocld  15462  mulcncflem  15757  plycolemc  15908  sincosq3sgn  15979  sincosq4sgn  15980  perfect1  16196  lgsdir2lem4  16248  lgsne0  16255  lgsquad2lem2  16299  2sqlem8a  16339  clwwlkext2edg  16761  bj-peano4  17079  iswomni0  17199