Theorem necon2ai 2672

Description: Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
necon2ai.1	|- ( A = B -> -. ph )

Assertion

Ref	Expression
necon2ai	|- ( ph -> A =/= B )

Proof of Theorem necon2ai

Step	Hyp	Ref	Expression
1		necon2ai.1	. . 3 |- ( A = B -> -. ph )
2	1	con2i 124	. 2 |- ( ph -> -. A = B )
3	2	neqned 2650	1 |- ( ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1452   =/= wne 2641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 190  df-ne 2643

This theorem is referenced by:  necon2i  2677  intex  4557  iin0  4575  opelopabsb  4711  0ellim  5492  inf3lem3  8153  cardmin2  8450  pm54.43  8452  canthp1lem2  9096  renepnf  9706  renemnf  9707  lt0ne0d  10200  nnne0  10664  hashnemnf  12565  hashnn0n0nn  12608  geolim  14003  geolim2  14004  georeclim  14005  geoisumr  14011  geoisum1c  14013  ramtcl2  15045  ramtcl2OLD  15046  lhop1  23045  logdmn0  23664  logcnlem3  23668  rusgranumwlkl1  25754  vcoprne  26279  strlem1  27984  subfacp1lem1  29974  rankeq1o  31009  poimirlem9  32013  poimirlem18  32022  poimirlem19  32023  poimirlem20  32024  poimirlem32  32036  fouriersw  38207  afvvfveq  38795  nn0nepnf  39229