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

Theorem sylanb 282
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 281 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  syl2anb  289  anabsan  564  2exeu  2091  eqtr2  2158  pm13.181  2390  rmob  3001  disjne  3416  seex  4257  tron  4304  fssres  5298  funbrfvb  5464  funopfvb  5465  fvelrnb  5469  fvco  5491  fvimacnvi  5534  ffvresb  5583  funresdfunsnss  5623  fvtp2g  5629  fvtp2  5632  fnex  5642  funex  5643  1st2nd  6079  dftpos4  6160  nnmsucr  6384  nnmcan  6415  xpmapenlem  6743  fundmfibi  6827  sup3exmid  8727  nzadd  9118  peano5uzti  9171  fnn0ind  9179  uztrn2  9355  irradd  9450  xltnegi  9630  xaddnemnf  9652  xaddnepnf  9653  xaddcom  9656  xnegdi  9663  elioore  9707  uzsubsubfz1  9840  fzo1fzo0n0  9972  elfzonelfzo  10019  qbtwnxr  10047  faclbnd  10499  faclbnd3  10501  dvdsprime  11814  restuni  12355  stoig  12356  cnnei  12415  tgioo  12729  divcnap  12738  bj-indind  13189
  Copyright terms: Public domain W3C validator