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

Theorem weqi 76
Description: Type of an equality. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
weqi.1 |- A:al
weqi.2 |- B:al
Assertion
Ref Expression
weqi |- [A = B]:*

Proof of Theorem weqi
StepHypRef Expression
1 weq 41 . 2 |- = :(al -> (al -> *))
2 weqi.1 . 2 |- A:al
3 weqi.2 . 2 |- B:al
41, 2, 3wov 72 1 |- [A = B]:*
Colors of variables: type var term
Syntax hints:  *hb 3   = ke 7  [kbr 9  wffMMJ2t 12
This theorem was proved from axioms:  ax-weq 40  ax-wov 71
This theorem is referenced by:  clf  115  ovl  117  wal  134  wan  136  wim  137  weu  141  alval  142  exval  143  euval  144  notval  145  imval  146  orval  147  anval  148  pm2.21  153  dfan2  154  ecase  163  exlimdv2  166  exlimdv  167  ax4e  168  eta  178  cbvf  179  leqf  181  exlimd  183  ac  197  exmid  199  ax8  211  ax9  212  ax10  213  ax11  214  ax12  215  ax13  216  ax14  217  axext  219  axrep  220  axpow  221  axun  222
  Copyright terms: Public domain W3C validator