Theorem mulne0

Description: The product of two nonzero numbers is nonzero. (Contributed by NM, 30-Dec-2007)

	Ref	Expression
Assertion	mulne0	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\to AB\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		mulne0b	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\left(A\ne 0\wedge B\ne 0\right)\leftrightarrow AB\ne 0\right)$$
2	1	biimpa	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(A\ne 0\wedge B\ne 0\right)\right)\to AB\ne 0$$
3	2	an4s	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\to AB\ne 0$$