Metamath Proof Explorer

Theorem dtrucor

Description: Corollary of dtru . This example illustrates the danger of blindly trusting the standard Deduction Theorem without accounting for free variables: the theorem form of this deduction is not valid, as shown by dtrucor2 . (Contributed by NM, 27-Jun-2002)

Ref Expression
Hypothesis dtrucor.1 x = y
Assertion dtrucor x y


Step Hyp Ref Expression
1 dtrucor.1 x = y
2 dtru ¬ x x = y
3 2 pm2.21i x x = y x y
4 3 1 mpg x y