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  1676  eqreu  2727  onsucsssucr  4200  ordsucunielexmid  4216  ovi3  5579  tfrlem9  5876  rdgon  5913  dom2lem  6188  distrlem4prl  6559  distrlem4pru  6560  recexprlemm  6595  aptisr  6685  renegcl  7048  remulext2  7364  mulext1  7376  apmul1  7526  nnge1  7698  0mnnnnn0  7970  nn0lt2  8078  zneo  8095  uzind2  8106  fzind  8109  nn0ind-raph  8111  elfzmlbp  8740  difelfznle  8743  elfzodifsumelfzo  8807  ssfzo12  8830
  Copyright terms: Public domain W3C validator