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

Theorem syl2anb 287
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 280 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2b 283 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylancb  412  stdcndc  813  reupick3  3325  difprsnss  3622  trin2  4886  imadiflem  5158  fnun  5185  fco  5244  f1co  5296  foco  5311  f1oun  5341  f1oco  5344  eqfunfv  5475  ftpg  5556  issmo  6137  tfrlem5  6163  ener  6625  domtr  6631  unen  6662  xpdom2  6676  mapen  6691  pm54.43  6993  axpre-lttrn  7613  axpre-mulgt0  7616  zmulcl  9005  qaddcl  9323  qmulcl  9325  rpaddcl  9360  rpmulcl  9361  rpdivcl  9362  xrltnsym  9466  xrlttri3  9470  ge0addcl  9651  ge0mulcl  9652  ge0xaddcl  9653  expclzaplem  10204  expge0  10216  expge1  10217  hashfacen  10466  qredeu  11618  nn0gcdsq  11717  iscn2  12205  txuni  12268  txcn  12280
  Copyright terms: Public domain W3C validator