Axiom ax-cb1 29

Description: A context has type boolean.

This and the next few axioms are not strictly necessary, and are conservative on any theorem for which every variable has a specified type, but by adding this axiom we can save some typehood hypotheses in many theorems. The easy way to see that this axiom is conservative is to note that every axiom and inference rule that constructs a theorem of the form R⊧A where R and A are type variables, also ensures that R:∗ and A:∗. Thus it is impossible to prove any theorem ⊢ R⊧A unless both ⊢ R:∗ and ⊢ A:∗ had been previously derived, so it is conservative to deduce ⊢ R:∗ from ⊢ R⊧A. The same remark applies to the construction of the theorem (A, B):∗- there is only one rule that creates a formula of this type, namely wct 48, and it requires that A:∗ and B:∗ be previously established, so it is safe to reverse the process in wctl 33 and wctr 34. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypothesis

Ref	Expression
ax-cb.1	⊢ R⊧A

Assertion

Ref	Expression
ax-cb1	⊢ R:∗

Detailed syntax breakdown of Axiom ax-cb1

Step	Hyp	Ref	Expression
1		hb 3	. 2 type ∗
2		tr	. 2 term R
3	1, 2	wffMMJ2t 12	1 wff R:∗

This axiom is referenced by:  mpdan  35  syldan  36  trul  39  wtru  43  eqcomx  52  ancoms  54  adantr  55  ct1  57  ct2  58  sylan  59  an32s  60  anasss  61  anassrs  62  dfov1  74  dfov2  75  eqtru  86  ceq1  89  ceq2  90  oveq123  98  oveq1  99  oveq12  100  oveq2  101  oveq  102  hbxfrf  107  hbxfr  108  hbth  109  hbc  110  hbov  111  hbl  112  insti  114  clf  115  ax4g  149  ax4  150  alrimiv  151  cla4v  152  dfan2  154  hbct  155  mpd  156  imp  157  ex  158  notnot1  160  con2d  161  ecase  163  exlimdv2  166  exlimdv  167  cbvf  179  leqf  181  alrimi  182  exlimd  183  alimdv  184  eximdv  185  alnex  186  isfree  188  ac  197  exmid  199  ax3  205  ax5  207  ax11  214  axext  219  axrep  220