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  2035  ceqsalt  2789  sbceqal  3045  csbiebt  3124  rspcsbela  3144  preqr1g  3796  repizf2  4195  copsexg  4277  onun2  4526  suc11g  4593  elrnrexdm  5701  isoselem  5867  riotass2  5904  oawordriexmid  6528  nnm00  6588  ecopovtrn  6691  ecopovtrng  6694  infglbti  7091  difinfsnlem  7165  enq0tr  7501  addnqprl  7596  addnqpru  7597  mulnqprl  7635  mulnqpru  7636  recexprlemss1l  7702  recexprlemss1u  7703  cauappcvgprlemdisj  7718  mulextsr1lem  7847  pitonn  7915  rereceu  7956  cnegexlem1  8201  ltadd2  8446  eqord2  8511  mulext  8641  mulgt1  8890  lt2halves  9227  addltmul  9228  nzadd  9378  ltsubnn0  9393  zextlt  9418  recnz  9419  zeo  9431  peano5uzti  9434  irradd  9720  irrmul  9721  xltneg  9911  xleadd1  9950  icc0r  10001  fznuz  10177  uznfz  10178  facndiv  10831  rennim  11167  abs00ap  11227  absle  11254  cau3lem  11279  caubnd2  11282  climshft  11469  subcn2  11476  mulcn2  11477  serf0  11517  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  efieq1re  11937  moddvds  11964  dvdsssfz1  12017  nn0seqcvgd  12209  algcvgblem  12217  eucalglt  12225  lcmgcdlem  12245  rpmul  12266  divgcdcoprm0  12269  isprm6  12315  rpexp  12321  eulerthlema  12398  eulerthlemh  12399  prmdiv  12403  pcprendvds2  12460  pcz  12501  pcprmpw  12503  pcadd2  12510  pcfac  12519  expnprm  12522  imasgrp2  13240  issubg4m  13323  znidomb  14214  tgss3  14314  cnpnei  14455  cnntr  14461  hmeoopn  14547  hmeocld  14548  mulcncflem  14843  plycolemc  14994  sincosq3sgn  15064  sincosq4sgn  15065  perfect1  15234  lgsdir2lem4  15272  lgsne0  15279  lgsquad2lem2  15323  2sqlem8a  15363  bj-peano4  15601  iswomni0  15695