Theorem dtrucor2 2764

Description: The theorem form of the deduction dtrucor 2763 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 1121	. 2 |- E.x x = y
2		dtrucor2.1	. . . . 5 |- (x = y -> x =/= y)
3	2	necon2bi 1604	. . . 4 |- (x = y -> -. x = y)
4		pm2.01 88	. . . 4 |- ((x = y -> -. x = y) -> -. x = y)
5	3, 4	ax-mp 7	. . 3 |- -. x = y
6	5	nex 1097	. 2 |- -. E.x x = y
7	1, 6	pm2.24ii 80	1 |- (ph /\ -. ph)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 953  E.wex 977   =/= wne 1577

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

This theorem depends on definitions:  df-bi 147  df-ex 978  df-ne 1579

Copyright terms: Public domain