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

Theorem sylanb 272
 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 117 . 2 (𝜑𝜓)
3 sylanb.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 271 1 ((𝜑𝜒) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  syl2anb  279  anabsan  517  2exeu  2008  eqtr2  2074  pm13.181  2302  rmob  2878  disjne  3301  seex  4100  tron  4147  fssres  5094  funbrfvb  5244  funopfvb  5245  fvelrnb  5249  fvco  5271  fvimacnvi  5309  ffvresb  5356  fvtp2g  5398  fvtp2  5401  fnex  5411  funex  5412  1st2nd  5835  dftpos4  5909  nnmsucr  6098  nnmcan  6123  nzadd  8354  peano5uzti  8405  fnn0ind  8413  uztrn2  8586  irradd  8678  xltnegi  8849  elioore  8882  uzsubsubfz1  9014  fzo1fzo0n0  9141  elfzonelfzo  9188  qbtwnxr  9214  faclbnd  9609  faclbnd3  9611  bj-indind  10443
 Copyright terms: Public domain W3C validator