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

Theorem sylbird 159
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbird.1
sylbird.2
Assertion
Ref Expression
sylbird

Proof of Theorem sylbird
StepHypRef Expression
1 sylbird.1 . . 3
21biimprd 147 . 2
3 sylbird.2 . 2
42, 3syld 40 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3imtr3d  191  drex1  1676  eqreu  2727  onsucsssucr  4199  ordsucunielexmid  4215  ovi3  5576  tfrlem9  5873  rdgon  5910  dom2lem  6181  distrlem4prl  6550  distrlem4pru  6551  recexprlemm  6586  aptisr  6657  renegcl  7020  remulext2  7336  mulext1  7348  apmul1  7498  nnge1  7669  0mnnnnn0  7940  nn0lt2  8047  zneo  8064  uzind2  8075  fzind  8078  nn0ind-raph  8080  elfzmlbp  8706  difelfznle  8709  elfzodifsumelfzo  8773  ssfzo12  8796
  Copyright terms: Public domain W3C validator