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

import proveit
from proveit import defaults
from proveit import A, B, C, D
from proveit.logic import Implies, Not, Or
from proveit.logic.booleans.disjunction  import left_in_bool, right_in_bool
left_in_bool.proof().disable(); right_in_bool.proof().disable() # disable these to avoid a longer proof
theory = proveit.Theory() # the theorem's theory

%proving destructive_dilemma

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

Prove by applying the constructive_dilemma after taking contraposing $A \Rightarrow C$ to $\lnot C \Rightarrow \lnot A$ and $B \Rightarrow D$ to $\lnot D \Rightarrow \lnot B$.

defaults.assumptions = destructive_dilemma.all_conditions()

defaults.assumptions:

Implies(A, C).contrapose()

,  ⊢  

Implies(B, D).contrapose()

,  ⊢  

Or(Not(C), Not(D)).derive_via_multi_dilemma(Or(Not(A), Not(B)))

, , , , , ,  ⊢  

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4, 5, 6, 7, 8, 9	, , , , , ,  ⊢
	: , : , : , :
2	conjecture		⊢
	proveit.logic.booleans.disjunction.constructive_dilemma
3	instantiation	12, 10	⊢
	:
4	instantiation	12, 11	⊢
	:
5	instantiation	12, 14	⊢
	:
6	instantiation	12, 17	⊢
	:
7	assumption		⊢
8	instantiation	15, 13, 14	,  ⊢
	: , :
9	instantiation	15, 16, 17	,  ⊢
	: , :
10	assumption		⊢
11	assumption		⊢
12	conjecture		⊢
	proveit.logic.booleans.negation.closure
13	assumption		⊢
14	assumption		⊢
15	theorem		⊢
	proveit.logic.booleans.implication.to_contraposition
16	assumption		⊢
17	assumption		⊢