Theorem necon2ai 2655

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 2633	1 |- ( ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1446   =/= wne 2624

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 189  df-ne 2626

This theorem is referenced by:  necon2i  2660  intex  4562  iin0  4580  opelopabsb  4714  0ellim  5488  inf3lem3  8140  cardmin2  8437  pm54.43  8439  canthp1lem2  9083  renepnf  9693  renemnf  9694  lt0ne0d  10186  nnne0  10649  hashnemnf  12534  hashnn0n0nn  12577  geolim  13938  geolim2  13939  georeclim  13940  geoisumr  13946  geoisum1c  13948  ramtcl2  14978  ramtcl2OLD  14979  lhop1  22978  logdmn0  23597  logcnlem3  23601  rusgranumwlkl1  25687  vcoprne  26210  strlem1  27915  subfacp1lem1  29914  rankeq1o  30950  poimirlem9  31961  poimirlem18  31970  poimirlem19  31971  poimirlem20  31972  poimirlem32  31984  fouriersw  38105  afvvfveq  38660  nn0nepnf  39089