In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving left_from_and
Under these presumptions, we begin our proof of
(see dependencies)
left_from_and may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

This is proven by simple generalization by the fact that extra conditions may always be added to derive a weaker statement.

In [3]:
proveit.logic.booleans.conjunction.left_from_and has been proven.
 step typerequirementsstatement
0generalization1  ⊢  
1assumption  ⊢