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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	logccne0d.0	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	logccne0d.1	⊢ ( 𝜑 → 𝐴 ≠ 1 )
Assertion	logccne0d	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		logccne0d.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		logccne0d.0	⊢ ( 𝜑 → 𝐴 ≠ 0 )
3		logccne0d.1	⊢ ( 𝜑 → 𝐴 ≠ 1 )
4		logccne0	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ≠ 0 )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ≠ 0 )