HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  eqtypri Unicode version
Definition eqtypri 71
Description: Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.)
Hypotheses
Ref Expression
eqtypri.1 |- A:al
eqtypri.2 |- R |= [B = A]
Assertion
Ref Expression
eqtypri |- B:al
Detailed syntax breakdown of Definition eqtypri
StepHypRef Expression
1 hal . 2 type al
2 tb . 2 term B
31, 2wffMMJ2t 12 1 wff B:al
Colors of variables: type var term
This definition is referenced by:  mpbir  77  3eqtr4i  86  hbc  100  wal  124  wfal  125  wan  126  wim  127  wnot  128  wex  129  wor  130  weu  131
  Copyright terms: Public domain W3C validator