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

Theorem syl2anb 289
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 282 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2b 285 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:  sylancb  415  stdcndc  831  reupick3  3365  difprsnss  3665  trin2  4937  imadiflem  5209  fnun  5236  fco  5295  f1co  5347  foco  5362  f1oun  5394  f1oco  5397  eqfunfv  5530  ftpg  5611  issmo  6192  tfrlem5  6218  ener  6680  domtr  6686  unen  6717  xpdom2  6732  mapen  6747  pm54.43  7062  axpre-lttrn  7715  axpre-mulgt0  7718  zmulcl  9130  qaddcl  9453  qmulcl  9455  rpaddcl  9493  rpmulcl  9494  rpdivcl  9495  xrltnsym  9608  xrlttri3  9612  ge0addcl  9793  ge0mulcl  9794  ge0xaddcl  9795  expclzaplem  10347  expge0  10359  expge1  10360  hashfacen  10610  qredeu  11812  nn0gcdsq  11912  cnovex  12402  iscn2  12406  txuni  12469  txcn  12481
  Copyright terms: Public domain W3C validator