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  6415  uzind3  8127  xrltnsym  8484  0fz1  8679  expivallem  8910  expival  8911  exp1  8915  expp1  8916
  Copyright terms: Public domain W3C validator