idt - Higher-Order Logic Explorer

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

Theorem idt 14

Description: The identity inference. (Contributed by Mario Carneiro, 9-Oct-2014.)

**Hypothesis**
Ref	Expression
idt.1	⊢ A:α

**Assertion**
Ref	Expression
idt	⊢ A:α

**Proof of Theorem idt**
Step	Hyp	Ref	Expression
1		idt.1	1 ⊢ A:α

Colors of variables: type var term

Syntax hints: wffMMJ2t 12

This theorem is referenced by: (None)