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

Theorem sylibd 148
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 143 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 45 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3imtr3d  201  dvelimdf  1969  ceqsalt  2686  sbceqal  2936  csbiebt  3009  rspcsbela  3029  preqr1g  3663  repizf2  4056  copsexg  4136  onun2  4376  suc11g  4442  elrnrexdm  5527  isoselem  5689  riotass2  5724  oawordriexmid  6334  nnm00  6393  ecopovtrn  6494  ecopovtrng  6497  infglbti  6880  difinfsnlem  6952  enq0tr  7210  addnqprl  7305  addnqpru  7306  mulnqprl  7344  mulnqpru  7345  recexprlemss1l  7411  recexprlemss1u  7412  cauappcvgprlemdisj  7427  mulextsr1lem  7556  pitonn  7624  rereceu  7665  cnegexlem1  7905  ltadd2  8149  eqord2  8214  mulext  8344  mulgt1  8589  lt2halves  8923  addltmul  8924  nzadd  9074  zextlt  9111  recnz  9112  zeo  9124  peano5uzti  9127  irradd  9406  irrmul  9407  xltneg  9587  xleadd1  9626  icc0r  9677  fznuz  9850  uznfz  9851  facndiv  10453  rennim  10742  abs00ap  10802  absle  10829  cau3lem  10854  caubnd2  10857  climshft  11041  subcn2  11048  mulcn2  11049  serf0  11089  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  efieq1re  11405  moddvds  11429  dvdsssfz1  11477  nn0seqcvgd  11649  algcvgblem  11657  eucalglt  11665  lcmgcdlem  11685  rpmul  11706  divgcdcoprm0  11709  isprm6  11752  rpexp  11758  tgss3  12174  cnpnei  12315  cnntr  12321  hmeoopn  12407  hmeocld  12408  mulcncflem  12686  sincosq3sgn  12836  sincosq4sgn  12837  bj-peano4  13080
  Copyright terms: Public domain W3C validator