Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > wctr | GIF version |
Description: Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.) |
Ref | Expression |
---|---|
wctl.1 | ⊢ (S, T):∗ |
Ref | Expression |
---|---|
wctr | ⊢ T:∗ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hb 3 | . 2 type ∗ | |
2 | tt | . 2 term T | |
3 | 1, 2 | wffMMJ2t 12 | 1 wff T:∗ |
Colors of variables: type var term |
This definition is referenced by: syldan 34 simpld 35 simprd 36 trul 37 ancoms 49 sylan 54 an32s 55 anassrs 57 ex 148 con2d 151 exlimdv 157 exlimd 171 alimdv 172 |
Copyright terms: Public domain | W3C validator |