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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving demorgans_law_and_to_or_bin_explicit

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
demorgans_law_and_to_or_bin_explicit:
(see dependencies)
In [3]:
%qed

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

Out[3]:
step typerequirementsstatement
0modus ponens1, 2
1instantiation3, 4, 5*
: , : , : , : , : , : , :
2instantiation6, 7, 8
: , :
3conjecture
proveit.logic.booleans.quantification.universality.bundle
4conjecture
proveit.numbers.numerals.decimals.posnat1
5instantiation9, 10, 11
: , : , : , :
6conjecture
proveit.logic.booleans.forall_over_bool_by_cases
7instantiation14, 12, 13
: , : , :
8instantiation14, 15, 16
: , : , :
9conjecture
proveit.core_expr_types.conditionals.condition_prepend_reduction
10conjecture
proveit.numbers.numerals.decimals.nat2
11instantiation17
: , :
12deduction18
13deduction19
14conjecture
proveit.logic.booleans.conditioned_forall_over_bool_by_cases
15deduction20
16instantiation21, 22
: , :
17conjecture
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
18theorem
proveit.logic.booleans.disjunction.true_or_true
19theorem
proveit.logic.booleans.disjunction.true_or_false
20theorem
proveit.logic.booleans.disjunction.false_or_true
21theorem
proveit.logic.booleans.implication.falsified_antecedent_implication
22instantiation23, 24
:
23theorem
proveit.logic.booleans.negation.double_negation_intro
24theorem
proveit.logic.booleans.negation.not_false
*equality replacement requirements