idi - Higher-Order Logic Explorer

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

Theorem idi 13

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

**Hypothesis**
Ref	Expression
idi.1	⊢ R⊧A

**Assertion**
Ref	Expression
idi	⊢ R⊧A

**Proof of Theorem idi**
Step	Hyp	Ref	Expression
1		idi.1	1 ⊢ R⊧A

Colors of variables: type var term

This proof depends on syntax axioms: ⊧wffMMJ2 11

This theorem is used by: (None)