P. 23 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2201-2300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abbid 2201	Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbidv 2202*	Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbi2dv 2203*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
Theorem	abbi1dv 2204*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)
Theorem	abid2 2205*	A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
Theorem	sb8ab 2206	Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ [𝑦 / 𝑥]𝜑}
Theorem	cbvab 2207	Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	cbvabv 2208*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	clelab 2209*	Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.)
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
Theorem	clabel 2210*	Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.)
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)))
Theorem	sbab 2211*	The right-hand side of the second equality is a way of representing proper substitution of 𝑦 for 𝑥 into a class variable. (Contributed by NM, 14-Sep-2003.)
⊢ (𝑥 = 𝑦 → 𝐴 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐴})
2.1.3  Class form not-free predicate
Syntax	wnfc 2212	Extend wff definition to include the not-free predicate for classes.
wff Ⅎ𝑥𝐴
Theorem	nfcjust 2213*	Justification theorem for df-nfc 2214. (Contributed by Mario Carneiro, 13-Oct-2016.)
⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴)
Definition	df-nfc 2214*	Define the not-free predicate for classes. This is read "𝑥 is not free in 𝐴". Not-free means that the value of 𝑥 cannot affect the value of 𝐴, e.g., any occurrence of 𝑥 in 𝐴 is effectively bound by a quantifier or something that expands to one (such as "there exists at most one"). It is defined in terms of the not-free predicate df-nf 1393 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfci 2215*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥 𝑦 ∈ 𝐴    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcii 2216*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcr 2217*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfcrii 2218*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
Theorem	nfcri 2219*	Consequence of the not-free predicate. (Note that unlike nfcr 2217, this does not require 𝑦 and 𝐴 to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
Theorem	nfcd 2220*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfceqi 2221	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
Theorem	nfcxfr 2222	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcxfrd 2223	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfceqdf 2224	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵))
Theorem	nfcv 2225*	If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴
Theorem	nfcvd 2226*	If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfab1 2227	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
Theorem	nfnfc1 2228	𝑥 is bound in Ⅎ𝑥𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥Ⅎ𝑥𝐴
Theorem	nfab 2229	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}
Theorem	nfaba1 2230	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑}
Theorem	nfnfc 2231	Hypothesis builder for Ⅎ𝑦𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Ⅎ𝑦𝐴
Theorem	nfeq 2232	Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel 2233	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfeq1 2234*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel1 2235*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfeq2 2236*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel2 2237*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfcrd 2238*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfeqd 2239	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Theorem	nfeld 2240	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)
Theorem	drnfc1 2241	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑦𝐵))
Theorem	drnfc2 2242	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝐴 ↔ Ⅎ𝑧𝐵))
Theorem	nfabd 2243	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓})
Theorem	dvelimdc 2244	Deduction form of dvelimc 2245. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑧𝐵)    &   ⊢ (𝜑 → (𝑧 = 𝑦 → 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵))
Theorem	dvelimc 2245	Version of dvelim 1938 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ (𝑧 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵)
Theorem	nfcvf 2246	If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
Theorem	nfcvf2 2247	If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. (Contributed by Mario Carneiro, 5-Dec-2016.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
Theorem	cleqf 2248	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2184. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	abid2f 2249	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.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
Theorem	sbabel 2250*	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.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]{𝑧 ∣ 𝜑} ∈ 𝐴 ↔ {𝑧 ∣ [𝑦 / 𝑥]𝜑} ∈ 𝐴)
2.1.4  Negated equality and membership
2.1.4.1  Negated equality
Syntax	wne 2251	Extend wff notation to include inequality.
wff 𝐴 ≠ 𝐵
Definition	df-ne 2252	Define inequality. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
Theorem	neii 2253	Inference associated with df-ne 2252. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐴 = 𝐵
Theorem	neir 2254	Inference associated with df-ne 2252. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐵
Theorem	nner 2255	Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
⊢ (𝐴 = 𝐵 → ¬ 𝐴 ≠ 𝐵)
Theorem	nnedc 2256	Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.)
⊢ (DECID 𝐴 = 𝐵 → (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	dcned 2257	Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
⊢ (𝜑 → DECID 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → DECID 𝐴 ≠ 𝐵)
Theorem	neqned 2258	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2272. One-way deduction form of df-ne 2252. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2301. (Revised by Wolf Lammen, 22-Nov-2019.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	neqne 2259	From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)
Theorem	neirr 2260	No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ ¬ 𝐴 ≠ 𝐴
Theorem	eqneqall 2261	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))
Theorem	dcne 2262	Decidable equality expressed in terms of ≠. Basically the same as df-dc 779. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))
Theorem	nonconne 2263	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
⊢ ¬ (𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵)
Theorem	neeq1 2264	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2 2265	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq1i 2266	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
Theorem	neeq2i 2267	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)
Theorem	neeq12i 2268	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)
Theorem	neeq1d 2269	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2d 2270	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq12d 2271	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))
Theorem	neneqd 2272	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
Theorem	neneq 2273	From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
Theorem	eqnetri 2274	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ≠ 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	eqnetrd 2275	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetrri 2276	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 ≠ 𝐶    ⇒   ⊢ 𝐵 ≠ 𝐶
Theorem	eqnetrrd 2277	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)
Theorem	neeqtri 2278	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrd 2279	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	neeqtrri 2280	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrrd 2281	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	syl5eqner 2282	B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	3netr3d 2283	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr4d 2284	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr3g 2285	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr4g 2286	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	necon3abii 2287	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
⊢ (𝐴 = 𝐵 ↔ 𝜑)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bbii 2288	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon3bii 2289	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)
Theorem	necon3abid 2290	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
Theorem	necon3bbid 2291	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))
Theorem	necon3bid 2292	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))
Theorem	necon3ad 2293	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓))
Theorem	necon3bd 2294	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))
Theorem	necon3d 2295	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))
Theorem	nesym 2296	Characterization of inequality in terms of reversed equality (see bicom 138). (Contributed by BJ, 7-Jul-2018.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
Theorem	nesymi 2297	Inference associated with nesym 2296. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐵 = 𝐴
Theorem	nesymir 2298	Inference associated with nesym 2296. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	necon3i 2299	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)
Theorem	necon3ai 2300	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)