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

Theorem sylanb 284
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 120 . 2 (𝜑𝜓)
3 sylanb.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 283 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  syl2anb  291  anabsan  575  2exeu  2129  eqtr2  2207  pm13.181  2441  rmob  3069  disjne  3490  seex  4349  tron  4396  fssres  5405  funbrfvb  5573  funopfvb  5574  fvelrnb  5578  fvco  5601  fvimacnvi  5645  ffvresb  5694  funresdfunsnss  5734  fvtp2g  5740  fvtp2  5743  fnex  5753  funex  5754  1st2nd  6199  dftpos4  6281  nnmsucr  6506  nnmcan  6537  xpmapenlem  6866  fundmfibi  6955  sup3exmid  8931  nzadd  9322  peano5uzti  9378  fnn0ind  9386  uztrn2  9562  irradd  9663  xltnegi  9852  xaddnemnf  9874  xaddnepnf  9875  xaddcom  9878  xnegdi  9885  elioore  9929  uzsubsubfz1  10065  fzo1fzo0n0  10200  elfzonelfzo  10247  qbtwnxr  10275  faclbnd  10738  faclbnd3  10740  dvdsprime  12139  pcgcd  12345  restuni  14055  stoig  14056  cnnei  14115  tgioo  14429  divcnap  14438  lgsdi  14821  bj-indind  15067
  Copyright terms: Public domain W3C validator