Theorem dedi 75

Description: Deduction theorem for equality.

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 40	. . 3 |- T.:*
3	1, 2	adantl 51	. 2 |- (T., S) |= T
4		dedi.2	. . 3 |- T |= S
5	4, 2	adantl 51	. 2 |- (T., T) |= S
6	3, 5	ded 74	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-refl 39  ax-eqmp 42  ax-ded 43  ax-ceq 46

This theorem depends on definitions:  df-ov 65

This theorem is referenced by:  dfan2  144  notval2  149  alnex  174  notnot  187