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

Axiom ax-cb2 30
Description: A theorem has type boolean. (This axiom is unnecessary; see ax-cb1 29.)
Hypothesis
Ref Expression
ax-cb.1 |- R |= A
Assertion
Ref Expression
ax-cb2 |- A:*

Detailed syntax breakdown of Axiom ax-cb2
StepHypRef Expression
1 hb 3 . 2 type *
2 ta . 2 term A
31, 2wffMMJ2t 12 1 wff A:*
Colors of variables: type var term
This axiom is referenced by:  simpld  35  simprd  36  mpbirx  48  mpbi  72  ded  74  eqtru  76  mpbir  77  hbth  99  alrimiv  141  mpd  146  ex  148  notval2  149  con3d  152  exlimdv2  156  exlimdv  157  alrimi  170  exlimd  171  eximdv  173  notnot  187  ax11  201
  Copyright terms: Public domain W3C validator