ax-eqmp - Higher-Order Logic Explorer

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

Axiom ax-eqmp 45

Description: Modus ponens for equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

**Hypotheses**
Ref	Expression
ax-eqmp.1	⊢ R⊧A
ax-eqmp.2	⊢ R⊧(( = A)B)

**Assertion**
Ref	Expression
ax-eqmp	⊢ R⊧B

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

Colors of variables: type var term

This axiom is referenced by: eqcomx 52 mpbirx 53 dfov1 74 mpbi 82