Dla przykładu zaprezentujemy dowód formuł 1. i 2. w rachunku INT:
Prawo identyczności {| cellspacing=15 | 1.
| Ax |- | 2. | | Ax |- | 3. | | reguła odrywania: 1,2 |- | 4. | | Ax |- | 5. | | reguła odrywania: 3,4
Słabe prawo podwójnego przeczenia {| cellspacing=15 | 1.
| Ax |- | 2. | | Ax |- | 3. | | reguła odrywania: 1,3 |- | 4. | | Ax |- | 5. | | reguła odrywania: 3,4 |- | 6. | | Ax |- | 7. | | reguła odrywania: 5,6
Narzędziem, które znakomicie przyspiesza proces dowodzenia, że pewne formuły są tezami INT jest następujące twierdzenie o dedukcji:
Twierdzenie o dedukcji
gdzie oznacza zbiór formuł dowodliwych w INT ze zbioru założeń
Jako ilustrację tego twierdzenia wykażemy dowodliwość w INT prawa przechodniości dla implikacji (p. 6. – wyżej):
1. reguła odrywania: 2. reguła odrywania: 3. twierdzenie o dedukcji 4. twierdzenie o dedukcji 5.