Theorem necon3bi 2958

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	⊢ (𝐴 = 𝐵 → 𝜑)

Assertion

Ref	Expression
necon3bi	⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem necon3bi

Step	Hyp	Ref	Expression
1		necon3bi.1	. . 3 ⊢ (𝐴 = 𝐵 → 𝜑)
2	1	con3i 154	. 2 ⊢ (¬ 𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 2939	1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  r19.2zb  4453  pwne  5298  alephord  9985  ackbij1lem18  10146  fin23lem26  10235  fin1a2lem6  10315  alephom  10496  gchxpidm  10580  egt2lt3  16131  nn0onn  16307  prmodvdslcmf  16975  chnccat  18549  symgfix2  19345  alexsubALTlem2  23992  alexsubALTlem4  23994  ptcmplem2  23997  nmoid  24686  cxplogb  26752  axlowdimlem17  29031  frgrncvvdeq  30384  hashxpe  32887  hasheuni  34242  fineqvnttrclse  35280  limsucncmpi  36639  matunitlindflem1  37813  poimirlem32  37849  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  dvasin  37901  lsat0cv  39289  unitscyglem4  42448  readvrec2  42612  readvrec  42613  pellexlem5  43071  uzfissfz  45567  xralrple2  45595  infxr  45607  icccncfext  46127  ioodvbdlimc1lem1  46171  volioc  46212  fourierdlem32  46379  fourierdlem49  46395  fourierdlem73  46419  fourierswlem  46470  fouriersw  46471  sge0pr  46634  voliunsge0lem  46712  carageniuncl  46763  isomenndlem  46770  hoimbl  46871