# Proof of proveit.logic.booleans.conjunction.left_from_and theorem¶

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
left_from_and:
(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]:
%qed

proveit.logic.booleans.conjunction.left_from_and has been proven.

Out[3]:
step typerequirementsstatement
0generalization1
1assumption