apply IsDeduct.mp_ Q
case h1.a.h1
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q} ∪ {Q.imp_ R}) R
case h1.a.h1.a
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q} ∪ {Q.imp_ R}) (Q.imp_ R)

case h1.a.h1.a
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q} ∪ {Q.imp_ R}) Q