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	|- ( ph -> A e. CC )
	logccne0d.0	|- ( ph -> A =/= 0 )
	logccne0d.1	|- ( ph -> A =/= 1 )
Assertion	logccne0d	|- ( ph -> ( log ` A ) =/= 0 )

Proof

Step	Hyp	Ref	Expression
1		logccne0d.a	|- ( ph -> A e. CC )
2		logccne0d.0	|- ( ph -> A =/= 0 )
3		logccne0d.1	|- ( ph -> A =/= 1 )
4		logccne0	|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) =/= 0 )
5	1 2 3 4	syl3anc	|- ( ph -> ( log ` A ) =/= 0 )