| ⊢ finite ⊃ (f ≡ g) ⇒ ⊢ f ≡ g | FiniteImpBfEqvBfRule |
Proof:
1 | finite ⊃ (f ≡ g) | Assump |
2 | finite ⊃ (f ⊃ g) | |
3 | f ⊃ g | |
4 | finite ⊃ (g ⊃ f) | |
5 | g ⊃ f | |
6 | f ≡ g |
qed
The next theorem’s proof involves the application of the previous derived inference rule together with completeness for PITL with just finite time: