p->(q->p)
(p->(p->q))->(p->q)
(p->(q->r))->(q->(p->r))
(p->q)->((q->r)->(p->r))
(¬q->¬p)->(p->q)
とmodus ponensからなる公理系(¬pはp->⊥の略記)の下で、
⊥->pと(p->(q->r))->((p->q)->(p->r))の導出手順を教えてください