Metamath Proof Explorer

Theorem mulne0

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

		Ref	Expression
	Assertion	mulne0	\|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A x. B ) =/= 0 )

Step	Hyp	Ref	Expression
1		mulne0b	\|- ( ( A e. CC /\ B e. CC ) -> ( ( A =/= 0 /\ B =/= 0 ) <-> ( A x. B ) =/= 0 ) )
2	1	biimpa	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( A x. B ) =/= 0 )
3	2	an4s	\|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A x. B ) =/= 0 )

Step

Hyp

Ref

Expression

 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A =/= 0 /\ B =/= 0 ) <-> ( A x. B ) =/= 0 ) )

 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( A x. B ) =/= 0 )

 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A x. B ) =/= 0 )