Theorem dtrucor2

Description: The theorem form of the deduction dtrucor leads to a contradiction, as mentioned in the "Wrong!" example at mmdeduction.html#bad . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 20-Oct-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	dtrucor2.1	$$⊢x=y\to x\ne y$$
Assertion	dtrucor2	$$⊢\left(\phi \wedge \neg \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dtrucor2.1	$$⊢x=y\to x\ne y$$
2		ax6e	$$⊢\exists xx=y$$
3	1	necon2bi	$$⊢x=y\to \neg x=y$$
4		pm2.01	$$⊢\left(x=y\to \neg x=y\right)\to \neg x=y$$
5	3 4	ax-mp	$$⊢\neg x=y$$
6	5	nex	$$⊢\neg \exists xx=y$$
7	2 6	pm2.24ii	$$⊢\left(\phi \wedge \neg \phi \right)$$