Theorem necon3bi 2820

Description: 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.)

Hypothesis

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

Assertion

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

Proof of Theorem necon3bi

Step	Hyp	Ref	Expression
1		necon3bi.1	. . 3 |- ( A = B -> ph )
2	1	con3i 150	. 2 |- ( -. ph -> -. A = B )
3	2	neqned 2801	1 |- ( -. ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

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 197  df-ne 2795

This theorem is referenced by:  r19.2zb  4061  pwne  4831  onnev  5848  alephord  8898  ackbij1lem18  9059  fin23lem26  9147  fin1a2lem6  9227  alephom  9407  gchxpidm  9491  egt2lt3  14934  prmodvdslcmf  15751  symgfix2  17836  chfacfisf  20659  chfacfisfcpmat  20660  alexsubALTlem2  21852  alexsubALTlem4  21854  ptcmplem2  21857  nmoid  22546  cxplogb  24524  axlowdimlem17  25838  frgrncvvdeq  27173  hasheuni  30147  limsucncmpi  32444  matunitlindflem1  33405  poimirlem32  33441  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  dvasin  33496  lsat0cv  34320  pellexlem5  37397  uzfissfz  39542  xralrple2  39570  infxr  39583  icccncfext  40100  ioodvbdlimc1lem1  40146  volioc  40188  fourierdlem32  40356  fourierdlem49  40372  fourierdlem73  40396  fourierswlem  40447  fouriersw  40448  prsal  40538  sge0pr  40611  voliunsge0lem  40689  carageniuncl  40737  isomenndlem  40744  hoimbl  40845