P. 26 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 2501-2600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfel2 2501*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ ℲxB    ⇒   ⊢ Ⅎx A ∈ B
Theorem	nfcrd 2502*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (φ → ℲxA)    ⇒   ⊢ (φ → Ⅎx y ∈ A)
Theorem	nfeqd 2503	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx A = B)
Theorem	nfeld 2504	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx A ∈ B)
Theorem	drnfc1 2505	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (∀x x = y → A = B)    ⇒   ⊢ (∀x x = y → (ℲxA ↔ ℲyB))
Theorem	drnfc2 2506	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (∀x x = y → A = B)    ⇒   ⊢ (∀x x = y → (ℲzA ↔ ℲzB))
Theorem	nfabd2 2507	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ ((φ ∧ ¬ ∀x x = y) → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx{y ∣ ψ})
Theorem	nfabd 2508	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx{y ∣ ψ})
Theorem	dvelimdc 2509	Deduction form of dvelimc 2510. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎxφ    &   ⊢ Ⅎzφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → ℲzB)    &   ⊢ (φ → (z = y → A = B))    ⇒   ⊢ (φ → (¬ ∀x x = y → ℲxB))
Theorem	dvelimc 2510	Version of dvelim 2016 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲzB    &   ⊢ (z = y → A = B)    ⇒   ⊢ (¬ ∀x x = y → ℲxB)
Theorem	nfcvf 2511	If x and y are distinct, then x is not free in y. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (¬ ∀x x = y → Ⅎxy)
Theorem	nfcvf2 2512	If x and y are distinct, then y is not free in x. (Contributed by Mario Carneiro, 5-Dec-2016.)
⊢ (¬ ∀x x = y → Ⅎyx)
Theorem	cleqf 2513	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
Theorem	abid2f 2514	A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 5-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    ⇒   ⊢ {x ∣ x ∈ A} = A
Theorem	sbabel 2515*	Theorem to move a substitution in and out of a class abstraction. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    ⇒   ⊢ ([y / x]{z ∣ φ} ∈ A ↔ {z ∣ [y / x]φ} ∈ A)
2.1.4  Negated equality and membership
Syntax	wne 2516	Extend wff notation to include inequality.
wff A ≠ B
Syntax	wnel 2517	Extend wff notation to include negated membership.
wff A ∉ B
Definition	df-ne 2518	Define inequality. (Contributed by NM, 5-Aug-1993.)
⊢ (A ≠ B ↔ ¬ A = B)
Definition	df-nel 2519	Define negated membership. (Contributed by NM, 7-Aug-1994.)
⊢ (A ∉ B ↔ ¬ A ∈ B)
Theorem	nne 2520	Negation of inequality. (Contributed by NM, 9-Jun-2006.)
⊢ (¬ A ≠ B ↔ A = B)
Theorem	neirr 2521	No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ ¬ A ≠ A
Theorem	exmidne 2522	Excluded middle with equality and inequality. (Contributed by NM, 3-Feb-2012.)
⊢ (A = B ∨ A ≠ B)
Theorem	nonconne 2523	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
⊢ ¬ (A = B ∧ A ≠ B)
Theorem	neeq1 2524	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
⊢ (A = B → (A ≠ C ↔ B ≠ C))
Theorem	neeq2 2525	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
⊢ (A = B → (C ≠ A ↔ C ≠ B))
Theorem	neeq1i 2526	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
⊢ A = B    ⇒   ⊢ (A ≠ C ↔ B ≠ C)
Theorem	neeq2i 2527	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
⊢ A = B    ⇒   ⊢ (C ≠ A ↔ C ≠ B)
Theorem	neeq12i 2528	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ≠ C ↔ B ≠ D)
Theorem	neeq1d 2529	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ≠ C ↔ B ≠ C))
Theorem	neeq2d 2530	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ≠ A ↔ C ≠ B))
Theorem	neeq12d 2531	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ≠ C ↔ B ≠ D))
Theorem	neneqd 2532	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ → A ≠ B)    ⇒   ⊢ (φ → ¬ A = B)
Theorem	eqnetri 2533	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A = B    &   ⊢ B ≠ C    ⇒   ⊢ A ≠ C
Theorem	eqnetrd 2534	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → B ≠ C)    ⇒   ⊢ (φ → A ≠ C)
Theorem	eqnetrri 2535	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A = B    &   ⊢ A ≠ C    ⇒   ⊢ B ≠ C
Theorem	eqnetrrd 2536	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → A ≠ C)    ⇒   ⊢ (φ → B ≠ C)
Theorem	neeqtri 2537	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A ≠ B    &   ⊢ B = C    ⇒   ⊢ A ≠ C
Theorem	neeqtrd 2538	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → B = C)    ⇒   ⊢ (φ → A ≠ C)
Theorem	neeqtrri 2539	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A ≠ B    &   ⊢ C = B    ⇒   ⊢ A ≠ C
Theorem	neeqtrrd 2540	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → C = B)    ⇒   ⊢ (φ → A ≠ C)
Theorem	syl5eqner 2541	B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
⊢ B = A    &   ⊢ (φ → B ≠ C)    ⇒   ⊢ (φ → A ≠ C)
Theorem	3netr3d 2542	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → A = C)    &   ⊢ (φ → B = D)    ⇒   ⊢ (φ → C ≠ D)
Theorem	3netr4d 2543	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → C = A)    &   ⊢ (φ → D = B)    ⇒   ⊢ (φ → C ≠ D)
Theorem	3netr3g 2544	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ A = C    &   ⊢ B = D    ⇒   ⊢ (φ → C ≠ D)
Theorem	3netr4g 2545	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
⊢ (φ → A ≠ B)    &   ⊢ C = A    &   ⊢ D = B    ⇒   ⊢ (φ → C ≠ D)
Theorem	necon3abii 2546	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
⊢ (A = B ↔ φ)    ⇒   ⊢ (A ≠ B ↔ ¬ φ)
Theorem	necon3bbii 2547	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (φ ↔ A = B)    ⇒   ⊢ (¬ φ ↔ A ≠ B)
Theorem	necon3bii 2548	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
⊢ (A = B ↔ C = D)    ⇒   ⊢ (A ≠ B ↔ C ≠ D)
Theorem	necon3abid 2549	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
⊢ (φ → (A = B ↔ ψ))    ⇒   ⊢ (φ → (A ≠ B ↔ ¬ ψ))
Theorem	necon3bbid 2550	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
⊢ (φ → (ψ ↔ A = B))    ⇒   ⊢ (φ → (¬ ψ ↔ A ≠ B))
Theorem	necon3bid 2551	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (A = B ↔ C = D))    ⇒   ⊢ (φ → (A ≠ B ↔ C ≠ D))
Theorem	necon3ad 2552	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (ψ → A = B))    ⇒   ⊢ (φ → (A ≠ B → ¬ ψ))
Theorem	necon3bd 2553	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (A = B → ψ))    ⇒   ⊢ (φ → (¬ ψ → A ≠ B))
Theorem	necon3d 2554	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
⊢ (φ → (A = B → C = D))    ⇒   ⊢ (φ → (C ≠ D → A ≠ B))
Theorem	necon3i 2555	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
⊢ (A = B → C = D)    ⇒   ⊢ (C ≠ D → A ≠ B)
Theorem	necon3ai 2556	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → A = B)    ⇒   ⊢ (A ≠ B → ¬ φ)
Theorem	necon3bi 2557	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (A = B → φ)    ⇒   ⊢ (¬ φ → A ≠ B)
Theorem	necon1ai 2558	Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.)
⊢ (¬ φ → A = B)    ⇒   ⊢ (A ≠ B → φ)
Theorem	necon1bi 2559	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (A ≠ B → φ)    ⇒   ⊢ (¬ φ → A = B)
Theorem	necon1i 2560	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (A ≠ B → C = D)    ⇒   ⊢ (C ≠ D → A = B)
Theorem	necon2ai 2561	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (A = B → ¬ φ)    ⇒   ⊢ (φ → A ≠ B)
Theorem	necon2bi 2562	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
⊢ (φ → A ≠ B)    ⇒   ⊢ (A = B → ¬ φ)
Theorem	necon2i 2563	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (A = B → C ≠ D)    ⇒   ⊢ (C = D → A ≠ B)
Theorem	necon2ad 2564	Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (A = B → ¬ ψ))    ⇒   ⊢ (φ → (ψ → A ≠ B))
Theorem	necon2bd 2565	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (φ → (ψ → A ≠ B))    ⇒   ⊢ (φ → (A = B → ¬ ψ))
Theorem	necon2d 2566	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
⊢ (φ → (A = B → C ≠ D))    ⇒   ⊢ (φ → (C = D → A ≠ B))
Theorem	necon1abii 2567	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.)
⊢ (¬ φ ↔ A = B)    ⇒   ⊢ (A ≠ B ↔ φ)
Theorem	necon1bbii 2568	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.)
⊢ (A ≠ B ↔ φ)    ⇒   ⊢ (¬ φ ↔ A = B)
Theorem	necon1abid 2569	Contrapositive deduction for inequality. (Contributed by NM, 21-Aug-2007.)
⊢ (φ → (¬ ψ ↔ A = B))    ⇒   ⊢ (φ → (A ≠ B ↔ ψ))
Theorem	necon1bbid 2570	Contrapositive inference for inequality. (Contributed by NM, 31-Jan-2008.)
⊢ (φ → (A ≠ B ↔ ψ))    ⇒   ⊢ (φ → (¬ ψ ↔ A = B))
Theorem	necon2abii 2571	Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.)
⊢ (A = B ↔ ¬ φ)    ⇒   ⊢ (φ ↔ A ≠ B)
Theorem	necon2bbii 2572	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (φ ↔ A ≠ B)    ⇒   ⊢ (A = B ↔ ¬ φ)
Theorem	necon2abid 2573	Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.)
⊢ (φ → (A = B ↔ ¬ ψ))    ⇒   ⊢ (φ → (ψ ↔ A ≠ B))
Theorem	necon2bbid 2574	Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (φ → (ψ ↔ A ≠ B))    ⇒   ⊢ (φ → (A = B ↔ ¬ ψ))
Theorem	necon4ai 2575	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (A ≠ B → ¬ φ)    ⇒   ⊢ (φ → A = B)
Theorem	necon4i 2576	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (A ≠ B → C ≠ D)    ⇒   ⊢ (C = D → A = B)
Theorem	necon4ad 2577	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (A ≠ B → ¬ ψ))    ⇒   ⊢ (φ → (ψ → A = B))
Theorem	necon4bd 2578	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (¬ ψ → A ≠ B))    ⇒   ⊢ (φ → (A = B → ψ))
Theorem	necon4d 2579	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (A ≠ B → C ≠ D))    ⇒   ⊢ (φ → (C = D → A = B))
Theorem	necon4abid 2580	Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008.)
⊢ (φ → (A ≠ B ↔ ¬ ψ))    ⇒   ⊢ (φ → (A = B ↔ ψ))
Theorem	necon4bbid 2581	Contrapositive law deduction for inequality. (Contributed by NM, 9-May-2012.)
⊢ (φ → (¬ ψ ↔ A ≠ B))    ⇒   ⊢ (φ → (ψ ↔ A = B))
Theorem	necon4bid 2582	Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.)
⊢ (φ → (A ≠ B ↔ C ≠ D))    ⇒   ⊢ (φ → (A = B ↔ C = D))
Theorem	necon1ad 2583	Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.)
⊢ (φ → (¬ ψ → A = B))    ⇒   ⊢ (φ → (A ≠ B → ψ))
Theorem	necon1bd 2584	Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (A ≠ B → ψ))    ⇒   ⊢ (φ → (¬ ψ → A = B))
Theorem	necon1d 2585	Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (A ≠ B → C = D))    ⇒   ⊢ (φ → (C ≠ D → A = B))
Theorem	neneqad 2586	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2532. One-way deduction form of df-ne 2518. (Contributed by David Moews, 28-Feb-2017.)
⊢ (φ → ¬ A = B)    ⇒   ⊢ (φ → A ≠ B)
Theorem	nebi 2587	Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.)
⊢ ((A = B ↔ C = D) ↔ (A ≠ B ↔ C ≠ D))
Theorem	pm13.18 2588	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((A = B ∧ A ≠ C) → B ≠ C)
Theorem	pm13.181 2589	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((A = B ∧ B ≠ C) → A ≠ C)
Theorem	pm2.21ddne 2590	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ (φ → A = B)    &   ⊢ (φ → A ≠ B)    ⇒   ⊢ (φ → ψ)
Theorem	pm2.61ne 2591	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (A = B → (ψ ↔ χ))    &   ⊢ ((φ ∧ A ≠ B) → ψ)    &   ⊢ (φ → χ)    ⇒   ⊢ (φ → ψ)
Theorem	pm2.61ine 2592	Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (A = B → φ)    &   ⊢ (A ≠ B → φ)    ⇒   ⊢ φ
Theorem	pm2.61dne 2593	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (A = B → ψ))    &   ⊢ (φ → (A ≠ B → ψ))    ⇒   ⊢ (φ → ψ)
Theorem	pm2.61dane 2594	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)
⊢ ((φ ∧ A = B) → ψ)    &   ⊢ ((φ ∧ A ≠ B) → ψ)    ⇒   ⊢ (φ → ψ)
Theorem	pm2.61da2ne 2595	Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.)
⊢ ((φ ∧ A = B) → ψ)    &   ⊢ ((φ ∧ C = D) → ψ)    &   ⊢ ((φ ∧ (A ≠ B ∧ C ≠ D)) → ψ)    ⇒   ⊢ (φ → ψ)
Theorem	pm2.61da3ne 2596	Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.)
⊢ ((φ ∧ A = B) → ψ)    &   ⊢ ((φ ∧ C = D) → ψ)    &   ⊢ ((φ ∧ E = F) → ψ)    &   ⊢ ((φ ∧ (A ≠ B ∧ C ≠ D ∧ E ≠ F)) → ψ)    ⇒   ⊢ (φ → ψ)
Theorem	necom 2597	Commutation of inequality. (Contributed by NM, 14-May-1999.)
⊢ (A ≠ B ↔ B ≠ A)
Theorem	necomi 2598	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
⊢ A ≠ B    ⇒   ⊢ B ≠ A
Theorem	necomd 2599	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
⊢ (φ → A ≠ B)    ⇒   ⊢ (φ → B ≠ A)
Theorem	neor 2600	Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)
⊢ ((A = B ∨ ψ) ↔ (A ≠ B → ψ))