| ⊢ | w1 ∧ f1 ⊃ g1 ; (w2 ∧ f2),…,⊢ wn−1 ∧ fn−1 ⊃ gn−1 ; (wn ∧ fn) | MultNestedChopImpChop | |
| ⇒ ⊢ w1 ∧ f1 ⊃ g1 ; … ; gn−1 ; (wn ∧ gn) |
The proof is by induction on n.
Proof for n = 1:
1 | ⊢ w1 ∧ f1 ⊃ w1 ∧ f1 |
qed
Proof for n > 1:
1 | ⊢ w1 ∧ f1 ⊃ g1 ; (w2 ∧ f2) | given |
2 | ⊢ wi ∧ fi ⊃ gi ; (wi+1 ∧ fi+1), for each i: 1 < i < n | given |
3 | ⊢ w2 ∧ f2 ⊃ g2 ; … ; gn−1 ; (wn ∧ gn) | 2, induction hypothesis |
4 | ⊢ w1 ∧ f1 ⊃ g1 ; g2 ; … ; gn−1 ; (wn ∧ gn) |
qed