I came across the following proof in the book *Logic*, by Paul Tomassi:

```

(P & Q) → ~R : R → (P → ~Q)

```

According to the author, the proof should be a simple application of *modus tollens*. The following is perhaps the most obvious way of proving it:

```

 1.   (P & Q) → ~R         Premise
 2.   R                    Assumption
 3.   ~~R                  Double Negative Ins.
 4.   ~(P & Q)             1,3 Modus Tollens
 5.   ~P ∨ ~Q              4 DeMorgen
 6.   P → ~Q               5 Implication Ident.
 7.   R → (P → ~Q)         2,6 Conditional Proof

```

The only problem is that the author hasn't yet introduced DeMorgen's identity or any other identities. The following is a list of all the resources that have so far been introduced:

* Conjunction Introduction & Elimination
* Conditional Introduction & Elimination (Modus Ponens)
* Biconditional Introduction & Elimination
* Double Negative Introduction & Elimination
* Modus Tollens

However, I don't see any way to do the proof without identity rules. The following is a possible strategy for trying to solve it without identies:

```

1.   (P & Q) → ~R         Premise
2.   R                    Assumption
3.   ~~R                  Double Negative Ins.
4.   ~(P & Q)             1,3 Modus Tollens
5.   ~(P → ~Q)            Assumption
...
15.  ~(P → ~Q) → (P & Q)  5,14 Conditional Proof
16.  P → ~Q               4,15 Modus Tollens
17.  R → (P → ~Q)         2,16 Conditional Proof

```

But I don't see how it's possible to get to my theoretical step 15 without deriving the identies from scratch. According to the author, the proof is possible in 11 steps.

How can it be done?