Description: Deduction version of nfiota . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfiotadw when possible. (Contributed by NM, 18-Feb-2013) (New usage is discouraged.)