ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylbird 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  1679  eqreu  2733  onsucsssucr  4235  ordsucunielexmid  4256  ovi3  5637  tfrlem9  5935  rdgon  5973  dom2lem  6252  distrlem4prl  6682  distrlem4pru  6683  recexprlemm  6722  caucvgprlem1  6777  caucvgprprlemexb  6805  aptisr  6863  renegcl  7272  remulext2  7591  mulext1  7603  apmul1  7764  nnge1  7937  0mnnnnn0  8214  nn0lt2  8322  zneo  8339  uzind2  8350  fzind  8353  nn0ind-raph  8355  ledivge1le  8652  elfzmlbp  8990  difelfznle  8993  elfzodifsumelfzo  9057  ssfzo12  9080  flqeqceilz  9160  addcn2  9831  mulcn2  9833  climrecvg1n  9867  algcvgblem  9888
  Copyright terms: Public domain W3C validator