Proof of proveit.logic.booleans.disjunction.demorgans_law_and_to_or_bin theorem

import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic import in_bool
from proveit.logic.booleans.disjunction import demorgans_law_and_to_or_bin_explicit 
theory = proveit.Theory() # the theorem's theory

%proving demorgans_law_and_to_or_bin

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

defaults.assumptions = demorgans_law_and_to_or_bin.all_conditions()

defaults.assumptions:

in_bool(defaults.assumptions[0].operands[0].operands[0].operand).prove()

 ⊢  

in_bool(defaults.assumptions[0].operands[0].operands[1].operand).prove()

 ⊢  

demorgans_law_and_to_or_bin_explicit

 ⊢  

demorgans_law_and_to_or_bin_explicit.instantiate(
    {A:A, B:B}, assumptions = demorgans_law_and_to_or_bin.all_conditions())

 ⊢  

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

%qed

proveit.logic.booleans.disjunction.demorgans_law_and_to_or_bin has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4, 13	⊢
	: , :
2	conjecture		⊢
	proveit.logic.booleans.disjunction.demorgans_law_and_to_or_bin_explicit
3	instantiation	10, 5	⊢
	:
4	instantiation	10, 6	⊢
	:
5	instantiation	7, 9	⊢
	: , :
6	instantiation	8, 9	⊢
	: , :
7	axiom		⊢
	proveit.logic.booleans.conjunction.left_in_bool
8	axiom		⊢
	proveit.logic.booleans.conjunction.right_in_bool
9	instantiation	10, 11	⊢
	:
10	axiom		⊢
	proveit.logic.booleans.negation.operand_is_bool
11	instantiation	12, 13	⊢
	:
12	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
13	assumption		⊢