| ⊢ | f ⊃ empty ∨ ( w ∧more) ; f ⇒ ⊢ w ∧ f ⊃ w | CSImpBox |
Proof:
1 | ⊢ f ⊃empty ∨ ( w ∧more) ; f | given |
2 | ⊢ w ∧¬ w ⊃¬empty | |
3 | ⊢ w ∧ f ∧¬ w ⊃ ( w ∧more) ; f | |
4 | ⊢ w ∧more ⊃ ( w ∧more) ∧fin w | |
5 | ⊢ ( w ∧more) ; f ⊃ (( w ∧more) ∧fin w) ; f | |
6 | ⊢ (( w ∧more) ∧fin w) ; f ≡ ( w ∧more) ; (w ∧ f) | |
7 | ⊢ ¬ w ⊃ ( w) ¬ w | |
8 | ⊢ ( w) ¬ w ⊃ ( w ∧more) ¬ w | |
9 | ⊢ ( w ∧more) ; (w ∧ f) ∧ ( w ∧more) ¬ w ⊃ |
|
( w ∧more) ; ((w ∧ f) ∧¬ w) | ||
10 | ⊢ (w ∧ f) ∧¬ w ⊃ ( w ∧more) ; ((w ∧ f) ∧¬ w) | |
11 | ⊢ ( w ∧more) ; ((w ∧ f) ∧¬ w) ⊃more ; ((w ∧ f) ∧¬ w) | |
12 | ⊢ (w ∧ f) ∧¬ w ⊃more ; ((w ∧ f) ∧¬ w) | |
13 | ⊢ w ∧ f ⊃ w |
qed