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=yxy
Assertion dtrucor2 φ¬φ

Proof

Step Hyp Ref Expression
1 dtrucor2.1 x=yxy
2 ax6e xx=y
3 1 necon2bi x=y¬x=y
4 pm2.01 x=y¬x=y¬x=y
5 3 4 ax-mp ¬x=y
6 5 nex ¬xx=y
7 2 6 pm2.24ii φ¬φ