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

Theorem sylbird 168
 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 156 . 2
3 sylbird.2 . 2
42, 3syld 44 1
 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  ax-ia2 105  ax-ia3 106 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  3imtr3d  200  drex1  1721  eqreu  2793  onsucsssucr  4281  ordsucunielexmid  4302  ovi3  5689  tfrlem9  5989  dom2lem  6341  distrlem4prl  6906  distrlem4pru  6907  recexprlemm  6946  caucvgprlem1  7001  caucvgprprlemexb  7029  aptisr  7087  renegcl  7506  addid0  7614  remulext2  7837  mulext1  7849  apmul1  8013  nnge1  8199  0mnnnnn0  8457  nn0lt2  8580  zneo  8599  uzind2  8610  fzind  8613  nn0ind-raph  8615  ledivge1le  8954  elfzmlbp  9290  difelfznle  9293  elfzodifsumelfzo  9357  ssfzo12  9380  flqeqceilz  9470  addmodlteq  9550  uzsinds  9588  facdiv  9832  facwordi  9834  bcpasc  9860  addcn2  10368  mulcn2  10370  climrecvg1n  10404  odd2np1  10498  oddge22np1  10506  gcdaddm  10600  algcvgblem  10656  cncongr1  10710
 Copyright terms: Public domain W3C validator