Theorem necon3bi 2954

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 2935	1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

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

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 2929

This theorem is referenced by:  r19.2zb  4446  pwne  5291  alephord  9963  ackbij1lem18  10124  fin23lem26  10213  fin1a2lem6  10293  alephom  10473  gchxpidm  10557  egt2lt3  16112  nn0onn  16288  prmodvdslcmf  16956  chnccat  18529  symgfix2  19326  alexsubALTlem2  23961  alexsubALTlem4  23963  ptcmplem2  23966  nmoid  24655  cxplogb  26721  axlowdimlem17  28934  frgrncvvdeq  30284  hashxpe  32784  hasheuni  34093  fineqvnttrclse  35132  limsucncmpi  36478  matunitlindflem1  37655  poimirlem32  37691  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  dvasin  37743  lsat0cv  39071  unitscyglem4  42230  readvrec2  42393  readvrec  42394  pellexlem5  42865  uzfissfz  45364  xralrple2  45392  infxr  45404  icccncfext  45924  ioodvbdlimc1lem1  45968  volioc  46009  fourierdlem32  46176  fourierdlem49  46192  fourierdlem73  46216  fourierswlem  46267  fouriersw  46268  sge0pr  46431  voliunsge0lem  46509  carageniuncl  46560  isomenndlem  46567  hoimbl  46668