Metamath Proof Explorer


Theorem nelaneqOLD

Description: Obsolete version of nelaneq as of 22-Apr-2026. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022) (Proof shortened by TM, 31-Dec-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nelaneqOLD ¬ A B A = B

Proof

Step Hyp Ref Expression
1 elirr ¬ A A
2 eleq2 A = B A A A B
3 1 2 mtbii A = B ¬ A B
4 3 con2i A B ¬ A = B
5 imnan A B ¬ A = B ¬ A B A = B
6 4 5 mpbi ¬ A B A = B