In [1]:

```
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
```

In [2]:

```
%proving constructive_dilemma
```

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.

In [3]:

```
defaults.assumptions = constructive_dilemma.all_conditions()
```

In [4]:

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

In [5]:

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

In [6]:

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

In [7]:

```
%qed
```

Out[7]: