Metamath Proof Explorer


Theorem nelbOLD

Description: Obsolete version of nelb as of 3-Nov-2024. (Contributed by Thierry Arnoux, 20-Nov-2023) (Proof shortened by SN, 23-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nelbOLD ¬ A B x B x A

Proof

Step Hyp Ref Expression
1 df-ne x A ¬ x = A
2 1 ralbii x B x A x B ¬ x = A
3 ralnex x B ¬ x = A ¬ x B x = A
4 2 3 bitri x B x A ¬ x B x = A
5 risset A B x B x = A
6 4 5 xchbinxr x B x A ¬ A B
7 6 bicomi ¬ A B x B x A