Theorem diveq1bd

Description: If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 . Converse of diveq1d . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	diveq1bd.1	|- ( ph -> B e. CC )
	diveq1bd.2	|- ( ph -> B =/= 0 )
	diveq1bd.3	|- ( ph -> A = B )
Assertion	diveq1bd	|- ( ph -> ( A / B ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		diveq1bd.1	|- ( ph -> B e. CC )
2		diveq1bd.2	|- ( ph -> B =/= 0 )
3		diveq1bd.3	|- ( ph -> A = B )
4	3 1	eqeltrd	|- ( ph -> A e. CC )
5	4 1 2	diveq1ad	|- ( ph -> ( ( A / B ) = 1 <-> A = B ) )
6	3 5	mpbird	|- ( ph -> ( A / B ) = 1 )