Proof of proveit.logic.booleans.implication.double_negate_consequent theorem

import proveit
theory = proveit.Theory() # the theorem's theory

%proving double_negate_consequent

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
double_negate_consequent:
(see dependencies)

double_negate_consequent.instance_expr.prove(
    assumptions=double_negate_consequent.conditions)

 ⊢  

double_negate_consequent may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed # automation can handle this one

proveit.logic.booleans.implication.double_negate_consequent has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	deduction	2	⊢
2	instantiation	3, 4	,  ⊢
	:
3	theorem		⊢
	proveit.logic.booleans.negation.double_negation_intro
4	modus ponens	5, 6	,  ⊢
5	assumption		⊢
6	assumption		⊢