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

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

import proveit.logic

%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)

# 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()

defaults.assumptions = not_right_if_neither.all_conditions()

defaults.assumptions:

AorB_given_B = Or(A, B).conclude_via_example(
    B, assumptions = defaults.assumptions + (B,))

AorB_given_B: ,  ⊢  

B_impl_AorB = AorB_given_B.as_implication(B)

B_impl_AorB:  ⊢  

B_impl_AorB.deny_antecedent()

 ⊢  

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

%qed

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

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