Theorem necon2ai 2638

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 120	. 2 |- ( ph -> -. A = B )
3	2	neqned 2606	1 |- ( ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1405   =/= wne 2598

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 185  df-ne 2600

This theorem is referenced by:  necon2i  2646  neneqadOLD  2712  intex  4549  iin0  4567  opelopabsb  4699  0ellim  5471  inf3lem3  8079  cardmin2  8410  pm54.43  8412  canthp1lem2  9060  renepnf  9670  renemnf  9671  lt0ne0d  10157  nnne0  10608  hashnemnf  12462  hashnn0n0nn  12505  geolim  13829  geolim2  13830  georeclim  13831  geoisumr  13837  geoisum1c  13839  ramtcl2  14736  lhop1  22705  logdmn0  23313  logcnlem3  23317  rusgranumwlkl1  25351  vcoprne  25872  strlem1  27568  subfacp1lem1  29463  rankeq1o  30496  fouriersw  37363  afvvfveq  37582