wctr - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > wctr		GIF version

Definition wctr 32

Description: Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.)

**Hypothesis**
Ref	Expression
wctl.1	⊢ (S, T):∗

**Assertion**
Ref	Expression
wctr	⊢ T:∗

**Detailed syntax breakdown of Definition wctr**
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