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

Theorem syl2anb 291
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 284 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2b 287 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:  sylancb  418  stdcndc  846  reupick3  3435  difprsnss  3745  trin2  5038  imadiflem  5314  fnun  5341  fco  5400  f1co  5452  foco  5467  f1oun  5500  f1oco  5503  eqfunfv  5639  ftpg  5721  issmo  6314  tfrlem5  6340  ener  6806  domtr  6812  unen  6843  xpdom2  6858  mapen  6875  pm54.43  7220  axpre-lttrn  7914  axpre-mulgt0  7917  zmulcl  9337  qaddcl  9667  qmulcl  9669  rpaddcl  9709  rpmulcl  9710  rpdivcl  9711  xrltnsym  9825  xrlttri3  9829  ge0addcl  10013  ge0mulcl  10014  ge0xaddcl  10015  expclzaplem  10578  expge0  10590  expge1  10591  hashfacen  10851  qredeu  12132  nn0gcdsq  12235  mul4sq  12429  cnovex  14173  iscn2  14177  txuni  14240  txcn  14252  lgsne0  14917  mul2sq  14941
  Copyright terms: Public domain W3C validator