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

In [1]:
import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic import in_bool, Not, Or
from proveit.logic.booleans.disjunction import not_left_if_neither
theory = proveit.Theory() # the theorem's theory

In [2]:
import proveit.logic

In [3]:
%proving not_right_if_neither

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
not_right_if_neither:
(see dependencies)
In [4]:
# If we do not disable "not_left_if_neither" then a sub-optimal derivation may be generated through the automration.
# (a locally optimal choice in minimizing proof steps is not always globally optimal)
not_left_if_neither.proof().disable()

In [5]:
defaults.assumptions = not_right_if_neither.all_conditions()

defaults.assumptions:
In [6]:
AorB_given_B = Or(A, B).conclude_via_example(
B, assumptions = defaults.assumptions + (B,))

AorB_given_B: ,  ⊢
In [7]:
B_impl_AorB = AorB_given_B.as_implication(B)

B_impl_AorB:
In [8]:
B_impl_AorB.deny_antecedent()

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

In [9]:
%qed

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

Out[9]:
step typerequirementsstatement
0generalization1
1instantiation2, 7, 3, 15
: , :
2theorem
proveit.logic.booleans.implication.modus_tollens_denial
3deduction4
4instantiation5, 6, 7, 8,  ⊢
: , :
5conjecture
proveit.logic.booleans.disjunction.or_if_right
6instantiation9, 11
: , :
7instantiation10, 11
: , :
8assumption
9axiom
proveit.logic.booleans.disjunction.left_in_bool
10axiom
proveit.logic.booleans.disjunction.right_in_bool
11instantiation12, 13
:
12axiom
proveit.logic.booleans.negation.operand_is_bool
13instantiation14, 15
:
14conjecture
proveit.logic.booleans.in_bool_if_true
15assumption