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

Theorem sylan2br 272
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2br.1 (χφ)
sylan2br.2 ((ψ χ) → θ)
Assertion
Ref Expression
sylan2br ((ψ φ) → θ)

Proof of Theorem sylan2br
StepHypRef Expression
1 sylan2br.1 . . 3 (χφ)
21biimpri 124 . 2 (φχ)
3 sylan2br.2 . 2 ((ψ χ) → θ)
42, 3sylan2 270 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:  syl2anbr  276  xordc1  1281  imainss  4682  xpexr2m  4705  funeu2  4870  imadiflem  4921  fnop  4945  ssimaex  5177  isosolem  5406  acexmidlem2  5452  fnovex  5481  smores3  5849  riinerm  6115  enq0sym  6414  uzind3  8087  xrltnsym  8444  0fz1  8639  expivallem  8870  expival  8871  exp1  8875  expp1  8876
  Copyright terms: Public domain W3C validator