IC3 Modulo Theories via Implicit Predicate Abstraction