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	⊢ ⊤⊧[S = T]

Proof of Theorem dedi

Step	Hyp	Ref	Expression
1		dedi.1	. . 3 ⊢ S⊧T
2		wtru 43	. . 3 ⊢ ⊤:∗
3	1, 2	adantl 56	. 2 ⊢ (⊤, S)⊧T
4		dedi.2	. . 3 ⊢ T⊧S
5	4, 2	adantl 56	. 2 ⊢ (⊤, T)⊧S
6	3, 5	ded 84	1 ⊢ ⊤⊧[S = T]

Syntax hints:   = ke 7  ⊤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