ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylanb 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  1992  eqtr2  2058  pm13.181  2284  rmob  2847  disjne  3270  seex  4060  tron  4088  fssres  5012  funbrfvb  5162  funopfvb  5163  fvelrnb  5167  fvco  5189  fvimacnvi  5227  ffvresb  5274  fvtp2g  5316  fvtp2  5319  fnex  5329  funex  5330  1st2nd  5752  dftpos4  5823  nnmsucr  6010  nnmcan  6032  peano5uzti  8214  fnn0ind  8222  uztrn2  8358  irradd  8447  xltnegi  8610  elioore  8643  uzsubsubfz1  8774  fzo1fzo0n0  8901  elfzonelfzo  8948  bj-indind  9499
  Copyright terms: Public domain W3C validator