Proof of proveit.logic.booleans.conjunction.binary_closure theorem

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

%proving binary_closure

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

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

%qed # conclude_as_folded automatically

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

	step type	requirements	statement
0	modus ponens	1, 2	⊢
1	instantiation	3, 4	⊢
	: , : , : , : , : , : , :
2	instantiation	9, 5, 6	⊢
	: , :
3	conjecture		⊢
	proveit.logic.booleans.quantification.universality.bundle
4	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
5	instantiation	9, 7, 8	⊢
	: , :
6	instantiation	9, 10, 11	⊢
	: , :
7	instantiation	21, 12	⊢
	:
8	instantiation	15, 13	⊢
	:
9	conjecture		⊢
	proveit.logic.booleans.forall_over_bool_by_cases
10	instantiation	15, 14	⊢
	:
11	instantiation	15, 16	⊢
	:
12	instantiation	17, 18	⊢
	:
13	instantiation	21, 19	⊢
	:
14	instantiation	21, 20	⊢
	:
15	axiom		⊢
	proveit.logic.booleans.negation.operand_is_bool
16	instantiation	21, 22	⊢
	:
17	axiom		⊢
	proveit.logic.booleans.eq_true_elim
18	axiom		⊢
	proveit.logic.booleans.conjunction.and_t_t
19	instantiation	25, 23	⊢
	:
20	instantiation	25, 24	⊢
	:
21	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
22	instantiation	25, 26	⊢
	:
23	axiom		⊢
	proveit.logic.booleans.conjunction.and_t_f
24	axiom		⊢
	proveit.logic.booleans.conjunction.and_f_t
25	theorem		⊢
	proveit.logic.booleans.negation.negation_intro
26	axiom		⊢
	proveit.logic.booleans.conjunction.and_f_f