## 4.4 Implication introduction

This is more interesting, since it allows doing something useful with hypothesis (those subdemonstrations which have a vertical bar to the left). It's:

And what it does mean is that if we supposed something (call it ), and we just discovered (by using the rules) that supposing made true (whatever it is), then we have something clear: we can't assure that always is true, but we can assure that implies , which is written .

This allows us to end the subdemonstration and continue working with what we were doing before. Remember that you can't finish natural deduction inside a subdemonstration.

Daniel Clemente Laboreo 2005-05-17