Theorem necon3bi 2955

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

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

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 2930

This theorem is referenced by:  r19.2zb  4445  pwne  5293  alephord  9973  ackbij1lem18  10134  fin23lem26  10223  fin1a2lem6  10303  alephom  10483  gchxpidm  10567  egt2lt3  16117  nn0onn  16293  prmodvdslcmf  16961  chnccat  18534  symgfix2  19330  alexsubALTlem2  23964  alexsubALTlem4  23966  ptcmplem2  23969  nmoid  24658  cxplogb  26724  axlowdimlem17  28938  frgrncvvdeq  30291  hashxpe  32794  hasheuni  34119  fineqvnttrclse  35165  limsucncmpi  36510  matunitlindflem1  37677  poimirlem32  37713  ovoliunnfl  37723  voliunnfl  37725  volsupnfl  37726  dvasin  37765  lsat0cv  39153  unitscyglem4  42312  readvrec2  42480  readvrec  42481  pellexlem5  42951  uzfissfz  45450  xralrple2  45478  infxr  45490  icccncfext  46010  ioodvbdlimc1lem1  46054  volioc  46095  fourierdlem32  46262  fourierdlem49  46278  fourierdlem73  46302  fourierswlem  46353  fouriersw  46354  sge0pr  46517  voliunsge0lem  46595  carageniuncl  46646  isomenndlem  46653  hoimbl  46754