Intro Natural Deduction Problem: Given premise (p -> q) -> p show p using deduction

Question

This is from the Daniel Bonevac Deduction text, page 122 #12.

Given premise (p -> q) -> p show p using deduction.

I can do this using made up rules on steps 4+5, not given in the book. The other steps are proper steps given in the book.

1. (p -> q) -> p.     A
2. Show p
3. | ¬p.              AIP
4. | ¬p -> ¬(p -> q)  made up rule. take contrapositive of conditional 1
5. | ¬(p -> q).       ->E, 4, 3
6. | ¬(¬p ∨ q).       made up rule. convert conditional 5 to disjunction form.
7. | (¬p ∨ q).        ∨I, 3

We've only covered conjunction exploitation/introduction, negation exploitation/introduction, indirect proof, reiteration, conditional exploitation, conditional proof, biconditional exploitation/introduction.

The fundamental rules covered:

&E: Conjunction Exploitation
&I: Conjunction Introduction
¬¬: Negation introduction/exploitation
AIP: Indirect Proof (Show p, then assume ¬p, derive contradiction, conclude and cancel Show)
R: Reiteration
->E: Conditional Exploitation
ACP: Conditional Proof (Show p->q, assume p, derive q, conclude and cancel Show)
I: Biconditional introduction
E: Biconditional exploitation

How could the the above proof be completed using only the given rules?

Answer 1

Hint

Assume [1] ¬p and [2] p; we have a contradiction and derive q. Thus, by →-intro, derive (p → q), discharging assumption [2].

Then derive è from premise and we have a new contradiction, concluding with p by Double Negation, discharging [1].

---

Addendum

Different systems have different implementations of the rules of inference (and 'exploitation' is not a common rule name), but the proof outlined above should generally look like:

 1.|_ (p -> q) -> p   Premise
 2.|  |_ ¬p           Assumption
 3.|  |  |_ p         Assumption
 4.|  |  |  |_ ¬q     Assumption
 5.|  |  |  |  p      Reiteration 3
 6.|  |  |  |  ¬p      Reiteration 2
 7.|  |  |  q         Indirect Proof 4-5,6 
 8.|  |  p -> q       Conditional Introduction 3-6
  .|  |  :            
  .|  |  :                         
  .|  p               Indirect Proof 2-?