dedi - Higher-Order Logic Explorer

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

Theorem dedi 75

Description: Deduction theorem for equality.

**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 40	. . 3 ⊢ ⊤:∗
3	1, 2	adantl 51	. 2 ⊢ (⊤, S)⊧T
4		dedi.2	. . 3 ⊢ T⊧S
5	4, 2	adantl 51	. 2 ⊢ (⊤, T)⊧S
6	3, 5	ded 74	1 ⊢ ⊤⊧[S = T]

Colors of variables: type var term

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-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