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

Step	Hyp	Ref	Expression
1		hb 3	. 2 type *
2		ta	. 2 term A
3	1, 2	wffMMJ2t 12	1 wff A:*

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