| ⊢ | f ≡ f | DaEqvDiDt |
Proof:
1 | ⊢ true ; f ≡ f | |
2 | ⊢ (true ; f) ; true ≡ ( f) ; true | |
3 | ⊢ (true ; f) ; true ≡ f | 2, def. of |
4 | ⊢ (true ; f) ; true ≡true ; f ; true | |
5 | ⊢ true ; f ; true ≡ f | |
6 | ⊢ f ≡ f | 5, def. of |
qed
Here is a corollary of theorems DaEqvDtDi and DaEqvDiDt: