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

Theorem sylbird 169
 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 157 . 2
3 sylbird.2 . 2
42, 3syld 45 1
 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  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  3imtr3d  201  drex1  1771  eqreu  2881  onsucsssucr  4434  ordsucunielexmid  4455  ovi3  5917  tfrlem9  6226  dom2lem  6676  distrlem4prl  7439  distrlem4pru  7440  recexprlemm  7479  caucvgprlem1  7534  caucvgprprlemexb  7562  aptisr  7634  map2psrprg  7660  renegcl  8070  addid0  8182  remulext2  8409  mulext1  8421  apmul1  8595  nnge1  8790  0mnnnnn0  9056  nn0lt2  9179  zneo  9199  uzind2  9210  fzind  9213  nn0ind-raph  9215  ledivge1le  9566  elfzmlbp  9963  difelfznle  9966  elfzodifsumelfzo  10032  ssfzo12  10055  flqeqceilz  10145  addmodlteq  10225  uzsinds  10269  facdiv  10539  facwordi  10541  bcpasc  10567  addcn2  11134  mulcn2  11136  climrecvg1n  11172  odd2np1  11629  oddge22np1  11637  gcdaddm  11731  algcvgblem  11789  cncongr1  11843  metss2lem  12728
 Copyright terms: Public domain W3C validator