cl - Higher-Order Logic Explorer

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

Theorem cl 106

Description: Evaluate a lambda expression.

**Assertion**
Ref	Expression
cl	⊢ ⊤⊧[(λx:α AC) = B]

Distinct variable groups: x,B x,C α,x

Proof of Theorem cl Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cl.1	. 2 ⊢ A:β
2		cl.2	. 2 ⊢ C:α
3		cl.3	. 2 ⊢ [x:α = C]⊧[A = B]
4	1, 3	eqtypi 69	. . 3 ⊢ B:β
5		wv 58	. . 3 ⊢ y:α:α
6	4, 5	ax-17 95	. 2 ⊢ ⊤⊧[(λx:α By:α) = B]
7	2, 5	ax-17 95	. 2 ⊢ ⊤⊧[(λx:α Cy:α) = C]
8	1, 2, 3, 6, 7	clf 105	1 ⊢ ⊤⊧[(λx:α AC) = B]

Colors of variables: type var term

Syntax hints: tv 1 kc 5 λkl 6 = ke 7 ⊤kt 8 [kbr 9 ⊧wffMMJ2 11 wffMMJ2t 12

This theorem was proved from axioms: ax-syl 15 ax-jca 17 ax-simpl 20 ax-simpr 21 ax-id 24 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-refl 39 ax-eqmp 42 ax-ceq 46 ax-beta 60 ax-distrc 61 ax-leq 62 ax-hbl1 93 ax-17 95 ax-inst 103

This theorem depends on definitions: df-ov 65

This theorem is referenced by: ovl 107 alval 132 exval 133 euval 134 notval 135 cla4v 142 dfan2 144 cla4ev 159 exmid 186 axpow 208