Theorem imadisjlnd

Description: Deduction form of one negated side of imadisj . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypothesis	imadisjlnd.1	|- ( ph -> ( dom A i^i B ) =/= (/) )
Assertion	imadisjlnd	|- ( ph -> ( A " B ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		imadisjlnd.1	|- ( ph -> ( dom A i^i B ) =/= (/) )
2		imadisj	|- ( ( A " B ) = (/) <-> ( dom A i^i B ) = (/) )
3	2	biimpi	|- ( ( A " B ) = (/) -> ( dom A i^i B ) = (/) )
4	3	necon3i	|- ( ( dom A i^i B ) =/= (/) -> ( A " B ) =/= (/) )
5	1 4	syl	|- ( ph -> ( A " B ) =/= (/) )