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

Theorem eqtypi 78
Description: Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) (Contributed by Mario Carneiro, 7-Oct-2014.)
Hypotheses
Ref Expression
eqcomi.1 |- A:al
eqcomi.2 |- R |= [A = B]
Assertion
Ref Expression
eqtypi |- B:al

Proof of Theorem eqtypi
StepHypRef Expression
1 eqcomi.1 . 2 |- A:al
2 eqcomi.2 . 2 |- R |= [A = B]
31, 2ax-eqtypi 77 1 |- B:al
Colors of variables: type var term
Syntax hints:   = ke 7  [kbr 9   |= wffMMJ2 11  wffMMJ2t 12
This theorem was proved from axioms:  ax-eqtypi 77
This theorem is referenced by:  eqcomi  79  mpbi  82  ceq12  88  leq  91  eqtri  95  3eqtr4i  96  3eqtr3i  97  oveq123  98  hbxfrf  107  clf  115  cl  116  cla4ev  169  cbvf  179  cbv  180  leqf  181  ac  197
  Copyright terms: Public domain W3C validator