Theorem logccne0d

Description: The logarithm isn't 0 if its argument isn't 0 or 1, deduction form. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	logccne0d.a	$$⊢\phi \to A\in ℂ$$
	logccne0d.0	$$⊢\phi \to A\ne 0$$
	logccne0d.1	$$⊢\phi \to A\ne 1$$
Assertion	logccne0d	$$⊢\phi \to \log A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		logccne0d.a	$$⊢\phi \to A\in ℂ$$
2		logccne0d.0	$$⊢\phi \to A\ne 0$$
3		logccne0d.1	$$⊢\phi \to A\ne 1$$
4		logccne0	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge A\ne 1\right)\to \log A\ne 0$$
5	1 2 3 4	syl3anc	$$⊢\phi \to \log A\ne 0$$