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

import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic import in_bool, Not, Or
theory = proveit.Theory() # the theorem's theory

%proving not_left_if_neither

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

defaults.assumptions = not_left_if_neither.all_conditions()

defaults.assumptions:

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

AorB_given_A: ,  ⊢  

A_impl_AorB = AorB_given_A.as_implication(A)

A_impl_AorB:  ⊢  

A_impl_AorB.deny_antecedent()

 ⊢  

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

%qed

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

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