Theorem dtrucor2 3519

Description: The theorem form of the deduction dtrucor 3518 leads to a contradiction, as mentioned in the "Wrong!" example at http://us.metamath.org/mpegif/mmdeduction.html#bad.

Hypothesis

Ref	Expression
dtrucor2.1	|- (x = y -> x =/= y)

Assertion

Ref	Expression
dtrucor2	|- (ph /\ -. ph)

Proof of Theorem dtrucor2

Step	Hyp	Ref	Expression
1		a9e 1483	. 2 |- E.x x = y
2		dtrucor2.1	. . . . 5 |- (x = y -> x =/= y)
3	2	necon2bi 2053	. . . 4 |- (x = y -> -. x = y)
4		pm2.01 104	. . . 4 |- ((x = y -> -. x = y) -> -. x = y)
5	3, 4	ax-mp 7	. . 3 |- -. x = y
6	5	nex 1456	. 2 |- -. E.x x = y
7	1, 6	pm2.24ii 96	1 |- (ph /\ -. ph)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   = wceq 1298  E.wex 1326   =/= wne 2017

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-9 1307

This theorem depends on definitions:  df-bi 164  df-ex 1327  df-ne 2019

Copyright terms: Public domain