Axiom ax-ded 46

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

Hypotheses

Ref	Expression
ax-ded.1	|- (R, S) |= T
ax-ded.2	|- (R, T) |= S

Assertion

Ref	Expression
ax-ded	|- R |= (( = S)T)

Detailed syntax breakdown of Axiom ax-ded

Step	Hyp	Ref	Expression
1		tr	. 2 term R
2		ke 7	. . . 4 term =
3		ts	. . . 4 term S
4	2, 3	kc 5	. . 3 term ( = S)
5		tt	. . 3 term T
6	4, 5	kc 5	. 2 term (( = S)T)
7	1, 6	wffMMJ2 11	1 wff R |= (( = S)T)

This axiom is referenced by:  ded  84