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

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
StepHypRef Expression
1 tr . 2 term R
2 ke 7 . . . 4 term =
3 ts . . . 4 term S
42, 3kc 5 . . 3 term ( = S)
5 tt . . 3 term T
64, 5kc 5 . 2 term (( = S)T)
71, 6wffMMJ2 11 1 wff R⊧(( = S)T)
Colors of variables: type var term
This axiom is referenced by:  ded  84
  Copyright terms: Public domain W3C validator