HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-inst Structured version   Unicode version

Axiom ax-inst 103
Description: Instantiate a theorem with a new term. The second and third hypotheses are the HOL equivalent of set.mm "effectively not free in" predicate (see set.mm's ax-17, or ax17 205).
Hypotheses
Ref Expression
ax-inst.1 |- R |= A
ax-inst.2 |- T. |= [(\x:al By:al) = B]
ax-inst.3 |- T. |= [(\x:al Sy:al) = S]
ax-inst.4 |- [x:al = C] |= [A = B]
ax-inst.5 |- [x:al = C] |= [R = S]
Assertion
Ref Expression
ax-inst |- S |= B
Distinct variable groups:   x,y   y,B   y,S

Detailed syntax breakdown of Axiom ax-inst
StepHypRef Expression
1 ts . 2 term S
2 tb . 2 term B
31, 2wffMMJ2 11 1 wff S |= B
Colors of variables: type var term
This axiom is referenced by:  insti  104  leqf  169  ax9  199
  Copyright terms: Public domain W3C validator