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

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  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