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

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

%proving constructive_dilemma

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

Prove by applying the singular_constructive_dilemma on $(C \lor D)$ as a unit, using or_if_left to prove $A \Rightarrow (C \lor D)$ and or_if_right to prove $B \Rightarrow (C \lor D)$ under the constructive_dilemma conditions.

defaults.assumptions = constructive_dilemma.all_conditions()

defaults.assumptions:

Or(C, D).conclude_via_example(C, assumptions = defaults.assumptions + (A,))

, , ,  ⊢  

Or(C, D).conclude_via_example(D, assumptions = defaults.assumptions + (B,))

, , ,  ⊢  

Or(A, B).derive_via_singular_dilemma(Or(C, D))

, , , , , ,  ⊢  

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4, 5, 6, 7	, , , , , ,  ⊢
	: , : , :
2	theorem		⊢
	proveit.logic.booleans.disjunction.singular_constructive_dilemma
3	assumption		⊢
4	assumption		⊢
5	assumption		⊢
6	deduction	8	, ,  ⊢
7	deduction	9	, ,  ⊢
8	instantiation	10, 13, 14, 11	, , ,  ⊢
	: , :
9	instantiation	12, 13, 14, 15	, , ,  ⊢
	: , :
10	conjecture		⊢
	proveit.logic.booleans.disjunction.or_if_left
11	modus ponens	16, 17	,  ⊢
12	conjecture		⊢
	proveit.logic.booleans.disjunction.or_if_right
13	assumption		⊢
14	assumption		⊢
15	modus ponens	18, 19	,  ⊢
16	assumption		⊢
17	assumption		⊢
18	assumption		⊢
19	assumption		⊢