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  2287  rmob  2850  disjne  3273  seex  4072  tron  4119  fssres  5066  funbrfvb  5216  funopfvb  5217  fvelrnb  5221  fvco  5243  fvimacnvi  5281  ffvresb  5328  fvtp2g  5370  fvtp2  5373  fnex  5383  funex  5384  1st2nd  5807  dftpos4  5878  nnmsucr  6067  nnmcan  6092  peano5uzti  8346  fnn0ind  8354  uztrn2  8490  irradd  8580  xltnegi  8748  elioore  8781  uzsubsubfz1  8912  fzo1fzo0n0  9039  elfzonelfzo  9086  bj-indind  10056
 Copyright terms: Public domain W3C validator