ImpliesQ[, ] tests whether the expression implies .
ImpliesQ returns False if it cannot determine whether implies , using any of its built-in transformation rules.
The related function Implies[, ] remains unevaluated if it cannot immediately determine whether implies .
See also: Implies, ImpliesRealQ, FullSimplify.
Note: this is an experimental feature, and in future versions of Mathematica it may not be supported, or may have a different specification.