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

Theorem sylanb 279
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 119 . 2 (𝜑𝜓)
3 sylanb.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 278 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  syl2anb  286  anabsan  543  2exeu  2047  eqtr2  2113  pm13.181  2344  rmob  2945  disjne  3355  seex  4186  tron  4233  fssres  5221  funbrfvb  5382  funopfvb  5383  fvelrnb  5387  fvco  5409  fvimacnvi  5452  ffvresb  5500  funresdfunsnss  5539  fvtp2g  5545  fvtp2  5548  fnex  5558  funex  5559  1st2nd  5989  dftpos4  6066  nnmsucr  6289  nnmcan  6318  xpmapenlem  6645  fundmfibi  6728  sup3exmid  8515  nzadd  8900  peano5uzti  8953  fnn0ind  8961  uztrn2  9135  irradd  9230  xltnegi  9401  xaddnemnf  9423  xaddnepnf  9424  xaddcom  9427  xnegdi  9434  elioore  9478  uzsubsubfz1  9611  fzo1fzo0n0  9743  elfzonelfzo  9790  qbtwnxr  9818  faclbnd  10280  faclbnd3  10282  dvdsprime  11547  restuni  12040  stoig  12041  cnnei  12099  tgioo  12336  bj-indind  12551
  Copyright terms: Public domain W3C validator