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  8122  fnn0ind  8130  uztrn2  8266  irradd  8355  xltnegi  8518  elioore  8551  uzsubsubfz1  8682  fzo1fzo0n0  8809  elfzonelfzo  8856  bj-indind  9391
 Copyright terms: Public domain W3C validator