| ⊢ (f ⊃ g) ⊃ f ⊃ g | BiImpDiImpDiSample |
Proof:
1 | true ⊃ true | |
2 | (true ⊃ true) | |
3 | (f ⊃ g) ∧ (true ⊃ true) |
|
⊃ (f ; true) ⊃ (g ; true) | ||
4 | (f ⊃ g) ⊃ (f ; true) ⊃ (g ; true) | |
5 | (f ⊃ g) ⊃ f ⊃ g | 4, def. of |
qed
The following instance of Axiom StateImpBi illustrates why it is not subsumed by Inference Rule BiGen:
| ⊢ ¬Q ⊃ ¬Q | ||
Here Q is a propositional variable. We cannot use BiGen since ¬Q is not a theorem.