| ⊢ | f1 ⊃ g1,…,⊢ fn ⊃ gn ⇒ ⊢ (f1 ; … ; fn) ⊃ (g1 ; …gn) | MultChopImpChop |
Proof is by induction on n.
Proof for n = 1:
1 | f1 ⊃ g1 | given |
qed
Proof for n > 1:
1 | ⊢ f1 ⊃ g1 | given |
2 | ⊢ fi ⊃ gi, for 2 ≤ i ≤ n | given |
3 | ⊢ (f2 ; … ; fn) ⊃ (g2 ; …gn) | 2,induction |
4 | ⊢ f1 ; f2 ; … ; fn ⊃ g1 ; g2 ; …gn |
qed