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

In [1]:
import proveit
from proveit import defaults
from proveit import C
from proveit.logic import TRUE, Equals
from proveit.logic.booleans.disjunction import singular_constructive_dilemma_lemma
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving singular_constructive_dilemma

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
singular_constructive_dilemma:
(see dependencies)
In [3]:
defaults.assumptions = singular_constructive_dilemma.all_conditions()

defaults.assumptions:

We will use the constrained singular constructive dilemma as a convenient Lemma to prove some $C=\top$ and deriving $C$ from there.

In [4]:
singular_constructive_dilemma_lemma

In [5]:
singular_constructive_dilemma_lemma.instantiate({C:Equals(C, TRUE)})

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

In [6]:
%qed

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

Out[6]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, , , ,  ⊢
:
2axiom
proveit.logic.booleans.eq_true_elim
3instantiation4, 5, 6, 7, 8, 9, 10, , , ,  ⊢
: , : , :
4theorem
proveit.logic.booleans.disjunction.singular_constructive_dilemma_lemma
5assumption
6assumption
7instantiation11
: , :
8assumption
9deduction12
10deduction13
11axiom
proveit.logic.equality.equality_in_bool
12instantiation15, 14,  ⊢
:
13instantiation15, 16,  ⊢
:
14modus ponens17, 18,  ⊢
15axiom
proveit.logic.booleans.eq_true_intro
16modus ponens19, 20,  ⊢
17assumption
18assumption
19assumption
20assumption