ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylibd Unicode version

Theorem sylibd 147
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
StepHypRef Expression
1 sylibd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylibd.2 . . 3  |-  ( ph  ->  ( ch  <->  th )
)
32biimpd 142 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 44 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3imtr3d  200  dvelimdf  1937  ceqsalt  2639  sbceqal  2883  csbiebt  2956  rspcsbela  2976  preqr1g  3593  repizf2  3971  copsexg  4044  onun2  4279  suc11g  4345  elrnrexdm  5395  isoselem  5554  riotass2  5589  oawordriexmid  6179  nnm00  6234  ecopovtrn  6335  ecopovtrng  6338  infglbti  6657  enq0tr  6930  addnqprl  7025  addnqpru  7026  mulnqprl  7064  mulnqpru  7065  recexprlemss1l  7131  recexprlemss1u  7132  cauappcvgprlemdisj  7147  mulextsr1lem  7262  pitonn  7322  rereceu  7361  cnegexlem1  7594  ltadd2  7834  mulext  8025  mulgt1  8252  lt2halves  8577  addltmul  8578  nzadd  8728  zextlt  8764  recnz  8765  zeo  8777  peano5uzti  8780  irradd  9056  irrmul  9057  xltneg  9223  icc0r  9269  fznuz  9439  uznfz  9440  facndiv  10036  rennim  10323  abs00ap  10383  absle  10410  cau3lem  10435  caubnd2  10438  climshft  10578  subcn2  10585  mulcn2  10586  serif0  10624  moddvds  10672  dvdsssfz1  10720  nn0seqcvgd  10890  algcvgblem  10898  eucalglt  10906  lcmgcdlem  10926  rpmul  10947  divgcdcoprm0  10950  isprm6  10993  rpexp  10999  bj-peano4  11280
  Copyright terms: Public domain W3C validator