| ⊢ | w ∧ f ⊃ g ; (w1 ∧ f1), ⊢ w1 ∧ f1 ⊃ g1 ; (w2 ∧ f2) | NestedChopImpChop | |
| ⇒ ⊢ w ∧ f ⊃ g ; g1 ; (w2 ∧ f2) |
Proof:
1 | ⊢ w ∧ f ⊃ g ; (w1 ∧ f1) | given |
2 | ⊢ w1 ∧ f1 ⊃ g1 ; (w2 ∧ f2) | given |
3 | ⊢ g ; (w1 ∧ f1) ⊃ g ; g1 ; (w2 ∧ f2) | |
4 | ⊢ w ∧ f ⊃ g ; g1 ; (w2 ∧ f2) |
qed