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

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

In [2]:
%proving neither_intro

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
neither_intro:
(see dependencies)
neither_intro may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

In [3]:
defaults.assumptions = neither_intro.all_conditions()

defaults.assumptions:
In [4]:
AeqF = A.evaluation()

AeqF:
In [5]:
BeqF = B.evaluation()

BeqF:
In [6]:
false_or_false_negated

In [7]:
AorF = AeqF.sub_left_side_into(false_or_false_negated.inner_expr().operand.operands[0],
auto_simplify=False)

AorF:
In [8]:
ForF = BeqF.sub_left_side_into(AorF, auto_simplify=False)

ForF: ,  ⊢
In [9]:
%qed

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

Out[9]:
step typerequirementsstatement
0generalization1
1instantiation4, 2, 3,  ⊢
: , :
2instantiation4, 5, 6
: , :
3assumption
4theorem
proveit.logic.equality.substitute_falsehood
5theorem
proveit.logic.booleans.disjunction.false_or_false_negated
6assumption