Description: Since the converse holds by a1i , this inference shows that we can
represent a not-free hypothesis with either F/ x ph (inference form)
or ( ph -> F/ x ph ) (deduction form). (Contributed by NM, 17-Aug-2018)(Proof shortened by Wolf Lammen, 10-Jul-2019)