This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \neq y$
	Assertion	dtrucor2	$⊢ (φ \land \neg φ)$

Proof

Step	Hyp	Ref	Expression
1		dtrucor2.1	$⊢ x = y \to x \neq y$
2		ax6e	$⊢ \exists x x = y$
3	1	necon2bi	$⊢ x = y \to \neg x = y$
4		pm2.01	$⊢ (x = y \to \neg x = y) \to \neg x = y$
5	3 4	ax-mp	$⊢ \neg x = y$
6	5	nex	$⊢ \neg \exists x x = y$
7	2 6	pm2.24ii	$⊢ (φ \land \neg φ)$