| ⊢ (g ≡ g1) ⊃ (f ⌢ g) ≡ (f ⌢ g1) | BoxChopEqvChop |
Proof:
1 | (g ≡ g1) ≡ (g ⊃ g1) ∧ (g1 ⊃ g) | |
2 | (g ⊃ g1) ⊃ (f ⌢ g) ⊃ (f ⌢ g1) | |
3 | (g1 ⊃ g) ⊃ (f ⌢ g1) ⊃ (f ⌢ g) | |
4 | (g ≡ g1) ⊃ (f ⌢ g) ≡ (f ⌢ g1) |
qed
The following derived variant of Inference Rule BfFGen omits the subformula finite: