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