# Proof of proveit.logic.booleans.disjunction.binary_closure theorem¶

In [1]:
import proveit
# we need to import false_or_false_negated to derive it's side-effects:
from proveit.logic.booleans.disjunction import \
(true_or_true, false_or_true, true_or_false, false_or_false_negated)
theory = proveit.Theory() # the theorem's theory

In [2]:
%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".

In [3]:
%qed

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

Out[3]:
step typerequirementsstatement
0modus ponens1, 2
1instantiation3, 4
: , : , : , : , : , : , :
2instantiation8, 5, 6
: , :
3conjecture
proveit.logic.booleans.quantification.universality.bundle
4conjecture
proveit.numbers.numerals.decimals.posnat1
5generalization7
6instantiation8, 9, 10
: , :
7instantiation19, 11
:
8conjecture
proveit.logic.booleans.forall_over_bool_by_cases
9instantiation19, 12
:
10instantiation13, 14
:
11instantiation15, 16, 17, 20
: , :
12theorem
proveit.logic.booleans.disjunction.false_or_true
13axiom
proveit.logic.booleans.negation.operand_is_bool
14instantiation19, 18
:
15conjecture
proveit.logic.booleans.disjunction.or_if_left
16instantiation19, 20
:
17assumption
18theorem
proveit.logic.booleans.disjunction.false_or_false_negated
19conjecture
proveit.logic.booleans.in_bool_if_true
20axiom
proveit.logic.booleans.true_axiom