| ⊢ | (w ⊃ fin w1) ; (w1 ⊃ fin w2) ⊃ (w ⊃ fin w2) | FinChopChain |
Proof:
1 | ⊢ w ∧ (w ⊃ fin w1) ; (w1 ⊃ fin w2) ⊃ |
|
(w ∧ (w ⊃ fin w1)) ; (w1 ⊃fin w2)) | ||
2 | ⊢ w ∧ (w ⊃ fin w1) ⊃fin w1 | |
3 | ⊢ (w ∧ (w ⊃ fin w1)) ; (w1 ⊃ fin w2) ⊃ |
|
(fin w1) ; (w1 ⊃ fin w2) | ||
4 | ⊢ (fin w1) ; (w1 ⊃ fin w2) ≡ (w1 ∧ (w1 ∧fin w2)) | |
5 | ⊢ (w1 ∧ (w1 ∧fin w2)) ⊃fin w2 | |
6 | ⊢ w ∧ (w ⊃ fin w1) ; (w1 ⊃ fin w2) ⊃fin w2 | |
7 | ⊢ (w ⊃ fin w1) ; (w1 ⊃ fin w2) ⊃ (w ⊃ fin w2) |
qed