Theorem necon3bi 2961

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  r19.2zb  4435  pwne  5288  alephord  9995  ackbij1lem18  10156  fin23lem26  10245  fin1a2lem6  10325  alephom  10506  gchxpidm  10590  egt2lt3  16171  nn0onn  16347  prmodvdslcmf  17016  chnccat  18590  symgfix2  19389  alexsubALTlem2  24038  alexsubALTlem4  24040  ptcmplem2  24043  nmoid  24732  cxplogb  26775  axlowdimlem17  29052  frgrncvvdeq  30404  hashxpe  32906  hasheuni  34276  fineqvnttrclse  35312  limsucncmpi  36680  matunitlindflem1  37990  poimirlem32  38026  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  dvasin  38078  lsat0cv  39532  unitscyglem4  42690  readvrec2  42845  readvrec  42846  pellexlem5  43285  uzfissfz  45778  xralrple2  45806  infxr  45818  icccncfext  46337  ioodvbdlimc1lem1  46381  volioc  46422  fourierdlem32  46589  fourierdlem49  46605  fourierdlem73  46629  fourierswlem  46680  fouriersw  46681  sge0pr  46844  voliunsge0lem  46922  carageniuncl  46973  isomenndlem  46980  hoimbl  47081