Theorem dedi 85

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

Hypotheses

Ref	Expression
dedi.1	|- S |= T
dedi.2	|- T |= S

Assertion

Ref	Expression
dedi	|- T. |= [S = T]

Proof of Theorem dedi

Step	Hyp	Ref	Expression
1		dedi.1	. . 3 |- S |= T
2		wtru 43	. . 3 |- T.:*
3	1, 2	adantl 56	. 2 |- (T., S) |= T
4		dedi.2	. . 3 |- T |= S
5	4, 2	adantl 56	. 2 |- (T., T) |= S
6	3, 5	ded 84	1 |- T. |= [S = T]

Syntax hints:   = ke 7  T.kt 8  [kbr 9   |= wffMMJ2 11

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-wctl 31  ax-wctr 32  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-ded 46  ax-wc 49  ax-ceq 51  ax-wov 71

This theorem depends on definitions:  df-ov 73

This theorem is referenced by:  dfan2  154  notval2  159  alnex  186  notnot  200