"Implied atomic propositions" in propositional boolean formula

Suppose we have a propositional boolean formula F and let M be the set of all models of that formula.

I am wondering if there is an efficient way to find all atomic propositions that are implied by the formula. Informally, this means that they can only have one specific value in all models M.

Does this problem have a specific name in literature? What is the complexity?

Examples:

Formula "(A)": the predicate A is implied by the formula, it can only ever have the truth value true in any model of the formula.

Formula "(A or B)": no predicate is implied by the formula, there are models where A is false, there are models where A is true, there are models where B is false, there are models where B is true.

Formula "A and (B or C)": in all models of this formula, A has to be true.

Suppose we had a TM $M$ which, given $F$ and some atomic $A$ occurring in $F$ it can efficiently (PTIME) decide whether all models of $F$ make $A$ true, i.e. whether $F \models A$.

Then we can efficiently decide the validity of any formula $G$ as follows.

Take $A$ to be any atom not in $G$. Craft $F := \lnot (G \land (\top \lor A))$, and use $M$ to decide if $F \models A$.

We then have
$$
(F \models A) \iff (F \models \bot) \iff \models \lnot F \iff \models G \land (\top \lor A) \iff \models G
$$

The first $\iff$ is nontrival, but easy to prove by considering the models where $A$ holds, and the others where $\lnot A$ holds, and exploiting our choice of $A$. It is left as an exercise ;-)

So, we constructed a polynomial reduction of validity to this problem.
Since validity is coNP hard, we deduce this problem is also coNP hard.

StackExchange Computer Science Q#77765, answer score: 5