ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylbird GIF 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-1 5  ax-2 6  ax-mp 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  1733  eqreu  2821  onsucsssucr  4354  ordsucunielexmid  4375  ovi3  5819  tfrlem9  6122  dom2lem  6569  distrlem4prl  7240  distrlem4pru  7241  recexprlemm  7280  caucvgprlem1  7335  caucvgprprlemexb  7363  aptisr  7421  renegcl  7840  addid0  7948  remulext2  8174  mulext1  8186  apmul1  8352  nnge1  8543  0mnnnnn0  8803  nn0lt2  8926  zneo  8946  uzind2  8957  fzind  8960  nn0ind-raph  8962  ledivge1le  9302  elfzmlbp  9692  difelfznle  9695  elfzodifsumelfzo  9761  ssfzo12  9784  flqeqceilz  9874  addmodlteq  9954  uzsinds  9997  facdiv  10261  facwordi  10263  bcpasc  10289  addcn2  10853  mulcn2  10855  climrecvg1n  10891  odd2np1  11300  oddge22np1  11308  gcdaddm  11402  algcvgblem  11458  cncongr1  11512  metss2lem  12283
  Copyright terms: Public domain W3C validator