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.) (Contributed by Mario Carneiro, 8-Oct-2014.)
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  37  simprd  38  mpbirx  53  mpbi  82  ded  84  eqtru  86  mpbir  87  hbth  109  alrimiv  151  mpd  156  ex  158  notval2  159  con3d  162  exlimdv2  166  exlimdv  167  alrimi  182  exlimd  183  eximdv  185  notnot  200  ax11  214
  Copyright terms: Public domain W3C validator