P. 27 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2601-2700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abbii 2601	Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 26-May-1993.)
|- ( ph <-> ps )   =>    |- { x | ph } = { x | ps }
Theorem	abbid 2602	Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x | ps } = { x | ch } )
Theorem	abbidv 2603*	Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x | ps } = { x | ch } )
Theorem	abbi2dv 2604*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
|- ( ph -> ( x e. A <-> ps ) )   =>    |- ( ph -> A = { x | ps } )
Theorem	abbi1dv 2605*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
|- ( ph -> ( ps <-> x e. A ) )   =>    |- ( ph -> { x | ps } = A )
Theorem	abbi1dvOLD 2606*	Obsolete proof of abbidv 2603 as of 16-Nov-2019. (Contributed by NM, 9-Jul-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps <-> x e. A ) )   =>    |- ( ph -> { x | ps } = A )
Theorem	abid2 2607*	A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)
|- { x | x e. A } = A
Theorem	cbvab 2608	Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
Theorem	cbvabOLD 2609	Obsolete proof of cbvab 2608 as of 16-Nov-2019. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
Theorem	cbvabv 2610*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
Theorem	clelab 2611*	Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
|- ( A e. { x | ph } <-> E. x ( x = A /\ ph ) )
Theorem	clelabOLD 2612*	Obsolete proof of clelab 2611 as of 16-Nov-2019. (Contributed by NM, 23-Dec-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. { x | ph } <-> E. x ( x = A /\ ph ) )
Theorem	clabel 2613*	Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.)
|- ( { x | ph } e. A <-> E. y ( y e. A /\ A. x ( x e. y <-> ph ) ) )
Theorem	sbab 2614*	The right-hand side of the second equality is a way of representing proper substitution of y for x into a class variable. (Contributed by NM, 14-Sep-2003.)
|- ( x = y -> A = { z | [ y / x ] z e. A } )
2.1.3  Class form not-free predicate
Syntax	wnfc 2615	Extend wff definition to include the not-free predicate for classes.
wff F/_ x A
Theorem	nfcjust 2616*	Justification theorem for df-nfc 2617. (Contributed by Mario Carneiro, 13-Oct-2016.)
|- ( A. y F/ x y e. A <-> A. z F/ x z e. A )
Definition	df-nfc 2617*	Define the not-free predicate for classes. This is read " x is not free in A". Not-free means that the value of x cannot affect the value of A, e.g., any occurrence of x in A is effectively bound by a "for all" or something that expands to one (such as "there exists"). It is defined in terms of the not-free predicate df-nf 1600 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_ x A <-> A. y F/ x y e. A )
Theorem	nfci 2618*	Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x y e. A   =>    |- F/_ x A
Theorem	nfcii 2619*	Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( y e. A -> A. x y e. A )   =>    |- F/_ x A
Theorem	nfcr 2620*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_ x A -> F/ x y e. A )
Theorem	nfcrii 2621*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- ( y e. A -> A. x y e. A )
Theorem	nfcri 2622*	Consequence of the not-free predicate. (Note that unlike nfcr 2620, this does not require y and A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- F/ x y e. A
Theorem	nfcd 2623*	Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ y ph   &    |- ( ph -> F/ x y e. A )   =>    |- ( ph -> F/_ x A )
Theorem	nfceqdf 2624	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/ x ph   &    |- ( ph -> A = B )   =>    |- ( ph -> ( F/_ x A <-> F/_ x B ) )
Theorem	nfceqi 2625	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
|- A = B   =>    |- ( F/_ x A <-> F/_ x B )
Theorem	nfceqiOLD 2626	Obsolete proof of nfceqi 2625 as of 16-Nov-2019. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A = B   =>    |- ( F/_ x A <-> F/_ x B )
Theorem	nfcxfr 2627	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   &    |- F/_ x B   =>    |- F/_ x A
Theorem	nfcxfrd 2628	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x A )
Theorem	nfcv 2629*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A
Theorem	nfcvd 2630*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )
Theorem	nfab1 2631	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x { x | ph }
Theorem	nfnfc1 2632	x is bound in F/_ x A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/_ x A
Theorem	nfab 2633	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/_ x { y | ph }
Theorem	nfaba1 2634	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { y | A. x ph }
Theorem	nfcrd 2635*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/ x y e. A )
Theorem	nfeqd 2636	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A = B )
Theorem	nfeld 2637	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A e. B )
Theorem	nfnfc 2638	Hypothesis builder for F/_ y A. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-13 1968. (Revised by Wolf Lammen, 10-Dec-2019.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	nfnfcALT 2639	Alternative, shorter proof of nfnfc 2638, based on more axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	nfeq 2640	Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A = B
Theorem	nfeqOLD 2641	Obsolete proof of nfeq 2640 as of 16-Nov-2019. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A = B
Theorem	nfel 2642	Hypothesis builder for elementhood. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e. B
Theorem	nfelOLD 2643	Obsolete proof of nfel 2642 as of 16-Nov-2019. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e. B
Theorem	nfeq1 2644*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A = B
Theorem	nfel1 2645*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A e. B
Theorem	nfeq2 2646*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A = B
Theorem	nfel2 2647*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A e. B
Theorem	drnfc1 2648	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- ( A. x x = y -> A = B )   =>    |- ( A. x x = y -> ( F/_ x A <-> F/_ y B ) )
Theorem	drnfc2 2649	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- ( A. x x = y -> A = B )   =>    |- ( A. x x = y -> ( F/_ z A <-> F/_ z B ) )
Theorem	nfabd2 2650	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ y ph   &    |- ( ( ph /\ -. A. x x = y ) -> F/ x ps )   =>    |- ( ph -> F/_ x { y | ps } )
Theorem	nfabd 2651	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/_ x { y | ps } )
Theorem	dvelimdc 2652	Deduction form of dvelimc 2653. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ x ph   &    |- F/ z ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/_ z B )   &    |- ( ph -> ( z = y -> A = B ) )   =>    |- ( ph -> ( -. A. x x = y -> F/_ x B ) )
Theorem	dvelimc 2653	Version of dvelim 2052 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/_ x A   &    |- F/_ z B   &    |- ( z = y -> A = B )   =>    |- ( -. A. x x = y -> F/_ x B )
Theorem	nfcvf 2654	If x and y are distinct, then x is not free in y. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- ( -. A. x x = y -> F/_ x y )
Theorem	nfcvf2 2655	If x and y are distinct, then y is not free in x. (Contributed by Mario Carneiro, 5-Dec-2016.)
|- ( -. A. x x = y -> F/_ y x )
Theorem	cleqf 2656	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2582. (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
Theorem	cleqfOLD 2657	Obsolete proof of cleqf 2656 as of 17-Nov-2019. (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
Theorem	abid2f 2658	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.) (Proof shortened by Wolf Lammen, 17-Nov-2019.)
|- F/_ x A   =>    |- { x | x e. A } = A
Theorem	abid2fOLD 2659	Obsolete proof of abid2f 2658 as of 17-Nov-2019. (Contributed by NM, 5-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/_ x A   =>    |- { x | x e. A } = A
Theorem	sbabel 2660*	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.) (Proof shortened by Wolf Lammen, 26-Dec-2019.)
|- F/_ x A   =>    |- ( [ y / x ] { z | ph } e. A <-> { z | [ y / x ] ph } e. A )
Theorem	sbabelOLD 2661*	Obsolete proof of sbabel 2660 as of 26-Dec-2019. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/_ x A   =>    |- ( [ y / x ] { z | ph } e. A <-> { z | [ y / x ] ph } e. A )
2.1.4  Negated equality and membership
Syntax	wne 2662	Extend wff notation to include inequality.
wff A =/= B
Syntax	wnel 2663	Extend wff notation to include negated membership.
wff A e/ B
Definition	df-ne 2664	Define inequality. (Contributed by NM, 26-May-1993.)
|- ( A =/= B <-> -. A = B )
Definition	df-nel 2665	Define negated membership. (Contributed by NM, 7-Aug-1994.)
|- ( A e/ B <-> -. A e. B )
2.1.4.1  Negated equality
Theorem	neii 2666	Inference associated with df-ne 2664. (Contributed by BJ, 7-Jul-2018.)
|- A =/= B   =>    |- -. A = B
Theorem	neir 2667	Inference associated with df-ne 2664. (Contributed by BJ, 7-Jul-2018.)
|- -. A = B   =>    |- A =/= B
Theorem	nne 2668	Negation of inequality. (Contributed by NM, 9-Jun-2006.)
|- ( -. A =/= B <-> A = B )
Theorem	neneqd 2669	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A =/= B )   =>    |- ( ph -> -. A = B )
Theorem	neqned 2670	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2669. One-way deduction form of df-ne 2664. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2696. (Revised by Wolf Lammen, 22-Nov-2019.)
|- ( ph -> -. A = B )   =>    |- ( ph -> A =/= B )
Theorem	neirr 2671	No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- -. A =/= A
Theorem	exmidne 2672	Excluded middle with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 17-Nov-2019.)
|- ( A = B \/ A =/= B )
Theorem	exmidneOLD 2673	Obsolete proof of exmidne 2672 as of 17-Nov-2019. (Contributed by NM, 3-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A = B \/ A =/= B )
Theorem	eqneqall 2674	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A = B -> ( A =/= B -> ph ) )
Theorem	nonconne 2675	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 21-Dec-2019.)
|- -. ( A = B /\ A =/= B )
Theorem	nonconneOLD 2676	Obsolete proof of nonconne 2675 as of 21-Dec-2019. (Contributed by NM, 3-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- -. ( A = B /\ A =/= B )
Theorem	necon3ad 2677	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( ps -> A = B ) )   =>    |- ( ph -> ( A =/= B -> -. ps ) )
Theorem	necon3adOLD 2678	Obsolete proof of necon3ad 2677 as of 23-Nov-2019. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> A = B ) )   =>    |- ( ph -> ( A =/= B -> -. ps ) )
Theorem	necon3bd 2679	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A = B -> ps ) )   =>    |- ( ph -> ( -. ps -> A =/= B ) )
Theorem	necon2ad 2680	Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( A = B -> -. ps ) )   =>    |- ( ph -> ( ps -> A =/= B ) )
Theorem	necon2adOLD 2681	Obsolete proof of necon2ad 2680 as of 23-Nov-2019. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( A = B -> -. ps ) )   =>    |- ( ph -> ( ps -> A =/= B ) )
Theorem	necon2bd 2682	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph -> ( ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> -. ps ) )
Theorem	necon1ad 2683	Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( -. ps -> A = B ) )   =>    |- ( ph -> ( A =/= B -> ps ) )
Theorem	necon1adOLD 2684	Obsolete proof of necon1ad 2683 as of 23-Nov-2019. (Contributed by NM, 2-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( -. ps -> A = B ) )   =>    |- ( ph -> ( A =/= B -> ps ) )
Theorem	necon1bd 2685	Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( A =/= B -> ps ) )   =>    |- ( ph -> ( -. ps -> A = B ) )
Theorem	necon1bdOLD 2686	Obsolete proof of necon1bd 2685 as of 23-Nov-2019. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( A =/= B -> ps ) )   =>    |- ( ph -> ( -. ps -> A = B ) )
Theorem	necon4ad 2687	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( A =/= B -> -. ps ) )   =>    |- ( ph -> ( ps -> A = B ) )
Theorem	necon4adOLD 2688	Obsolete proof of necon4ad 2687 as of 23-Nov-2019. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( A =/= B -> -. ps ) )   =>    |- ( ph -> ( ps -> A = B ) )
Theorem	necon4bd 2689	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( -. ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> ps ) )
Theorem	necon4bdOLD 2690	Obsolete proof of necon4bd 2689 as of 23-Nov-2019. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( -. ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> ps ) )
Theorem	necon3d 2691	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
|- ( ph -> ( A = B -> C = D ) )   =>    |- ( ph -> ( C =/= D -> A =/= B ) )
Theorem	necon1d 2692	Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A =/= B -> C = D ) )   =>    |- ( ph -> ( C =/= D -> A = B ) )
Theorem	necon2d 2693	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
|- ( ph -> ( A = B -> C =/= D ) )   =>    |- ( ph -> ( C = D -> A =/= B ) )
Theorem	necon4d 2694	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A =/= B -> C =/= D ) )   =>    |- ( ph -> ( C = D -> A = B ) )
Theorem	necon3ai 2695	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A = B )   =>    |- ( A =/= B -> -. ph )
Theorem	necon3bi 2696	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
|- ( A = B -> ph )   =>    |- ( -. ph -> A =/= B )
Theorem	necon3biOLD 2697	Obsolete proof of necon3bi 2696 as of 22-Nov-2019. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A = B -> ph )   =>    |- ( -. ph -> A =/= B )
Theorem	necon1ai 2698	Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
|- ( -. ph -> A = B )   =>    |- ( A =/= B -> ph )
Theorem	necon1aiOLD 2699	Obsolete proof of necon1ai 2698 as of 22-Nov-2019. (Contributed by NM, 12-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. ph -> A = B )   =>    |- ( A =/= B -> ph )
Theorem	necon1bi 2700	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
|- ( A =/= B -> ph )   =>    |- ( -. ph -> A = B )