ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylbird Structured version   GIF 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  1653  eqreu  2702  onsucsssucr  4173  ordsucunielexmid  4189  ovi3  5549  tfrlem9  5846  rdgon  5882  distrlem4prl  6410  distrlem4pru  6411  recexprlemm  6446  aptisr  6516  renegcl  6872  remulext2  7188  mulext1  7200  apmul1  7350  nnge1  7521  0mnnnnn0  7789  nn0lt2  7888  zneo  7905  uzind2  7916  fzind  7919  nn0ind-raph  7921
  Copyright terms: Public domain W3C validator