ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylanb Structured version   GIF version

Theorem sylanb 268
Description: A syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
sylanb.1 (φψ)
sylanb.2 ((ψ χ) → θ)
Assertion
Ref Expression
sylanb ((φ χ) → θ)

Proof of Theorem sylanb
StepHypRef Expression
1 sylanb.1 . . 3 (φψ)
21biimpi 113 . 2 (φψ)
3 sylanb.2 . 2 ((ψ χ) → θ)
42, 3sylan 267 1 ((φ χ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  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:  syl2anb  275  anabsan  509  2exeu  1989  eqtr2  2055  pm13.181  2281  rmob  2844  disjne  3267  seex  4057  tron  4085  fssres  5009  funbrfvb  5159  funopfvb  5160  fvelrnb  5164  fvco  5186  fvimacnvi  5224  ffvresb  5271  fvtp2g  5313  fvtp2  5316  fnex  5326  funex  5327  1st2nd  5749  dftpos4  5819  nnmsucr  6006  nnmcan  6028  peano5uzti  8082  fnn0ind  8090  uztrn2  8226  irradd  8315  xltnegi  8478  elioore  8511  uzsubsubfz1  8642  fzo1fzo0n0  8769  elfzonelfzo  8816
  Copyright terms: Public domain W3C validator