ax-id - Higher-Order Logic Explorer

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

Axiom ax-id 24

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

**Hypothesis**
Ref	Expression
ax-id.1	⊢ R:∗

**Assertion**
Ref	Expression
ax-id	⊢ R⊧R

**Detailed syntax breakdown of Axiom ax-id**
Step	Hyp	Ref	Expression
1		tr	. 2 term R
2	1, 1	wffMMJ2 11	1 wff R⊧R

Colors of variables: type var term

This axiom is referenced by: id 25 19.8a 170