Theorem necon3bi 2984

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 155	. 2 ⊢ (¬ 𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 2965	1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  r19.2zb  4462  pwne  5325  alephord  10060  ackbij1lem18  10220  fin23lem26  10310  fin1a2lem6  10390  alephom  10571  gchxpidm  10655  egt2lt3  16263  nn0onn  16439  prmodvdslcmf  17108  chnccat  18683  symgfix2  19487  alexsubALTlem2  24186  alexsubALTlem4  24188  ptcmplem2  24191  nmoid  24880  cxplogb  26929  axlowdimlem17  29286  frgrncvvdeq  30638  hashxpe  33130  hasheuni  34453  fineqvnttrclse  35515  limsucncmpi  36934  matunitlindflem1  38245  poimirlem32  38281  ovoliunnfl  38291  voliunnfl  38293  volsupnfl  38294  dvasin  38333  lsat0cv  39785  unitscyglem4  42943  readvrec2  43100  readvrec  43101  pellexlem5  43540  uzfissfz  46022  xralrple2  46050  infxr  46062  icccncfext  46581  ioodvbdlimc1lem1  46625  volioc  46666  fourierdlem32  46833  fourierdlem49  46849  fourierdlem73  46873  fourierswlem  46924  fouriersw  46925  sge0pr  47088  voliunsge0lem  47166  carageniuncl  47217  isomenndlem  47224  hoimbl  47325