HigherOrder Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > HOLE Home > Th. List > axded  Unicode version 
Description: Deduction theorem for equality. 
Ref  Expression 

axded.1  
axded.2 
Ref  Expression 

axded 
Step  Hyp  Ref  Expression 

1  tr  . 2 term  
2  ke 7  . . . 4 term  
3  ts  . . . 4 term  
4  2, 3  kc 5  . . 3 term 
5  tt  . . 3 term  
6  4, 5  kc 5  . 2 term 
7  1, 6  wffMMJ2 11  1 wff 
Colors of variables: type var term 
This axiom is referenced by: ded 74 
Copyright terms: Public domain  W3C validator 