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

Theorem syl2anb 279
Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
Hypotheses
Ref Expression
syl2anb.1 (𝜑𝜓)
syl2anb.2 (𝜏𝜒)
syl2anb.3 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
syl2anb ((𝜑𝜏) → 𝜃)

Proof of Theorem syl2anb
StepHypRef Expression
1 syl2anb.2 . 2 (𝜏𝜒)
2 syl2anb.1 . . 3 (𝜑𝜓)
3 syl2anb.3 . . 3 ((𝜓𝜒) → 𝜃)
42, 3sylanb 272 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2b 275 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:  sylancb  403  reupick3  3250  difprsnss  3530  trin2  4744  imadiflem  5006  fnun  5033  fco  5084  f1co  5129  foco  5144  f1oun  5174  f1oco  5177  eqfunfv  5298  ftpg  5375  issmo  5934  tfrlem5  5961  ener  6290  domtr  6296  unen  6324  xpdom2  6336  axpre-lttrn  7016  axpre-mulgt0  7019  zmulcl  8355  qaddcl  8667  qmulcl  8669  rpaddcl  8704  rpmulcl  8705  rpdivcl  8706  xrltnsym  8815  xrlttri3  8819  ge0addcl  8951  ge0mulcl  8952  serige0  9417  expclzaplem  9444  expge0  9456  expge1  9457
  Copyright terms: Public domain W3C validator