The following wffs are instances of axioms that are used in the propositional calculus.
Implication introduction: P implies (Q implies P)
Implication distribution: (P implies (Q implies R)) implies ((P implies Q) implies (P implies R))
Contradiction realization: (Q impies ~P) implies ((Q implies P) implies ~Q)
Use resolution refutation to prove each of these formulas.