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

In [1]:
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

In [2]:
%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)
In [3]:
defaults.assumptions = not_left_if_neither.all_conditions()

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

AorB_given_A: ,  ⊢
In [5]:
A_impl_AorB = AorB_given_A.as_implication(A)

A_impl_AorB:
In [6]:
A_impl_AorB.deny_antecedent()

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

In [7]:
%qed

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

Out[7]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, 4, 16
: , :
2theorem
proveit.logic.booleans.implication.modus_tollens_denial
3instantiation5, 12
: , :
4deduction6
5axiom
proveit.logic.booleans.disjunction.left_in_bool
6instantiation7, 8, 9, 10,  ⊢
: , :
7conjecture
proveit.logic.booleans.disjunction.or_if_left
8instantiation15, 10
:
9instantiation11, 12
: , :
10assumption
11axiom
proveit.logic.booleans.disjunction.right_in_bool
12instantiation13, 14
:
13axiom
proveit.logic.booleans.negation.operand_is_bool
14instantiation15, 16
:
15conjecture
proveit.logic.booleans.in_bool_if_true
16assumption