Theorem necon3bd 3001

Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

Ref	Expression
necon3bd.1	⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))

Assertion

Ref	Expression
necon3bd	⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Proof of Theorem necon3bd

Step	Hyp	Ref	Expression
1		nne 2991	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
2		necon3bd.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3	1, 2	syl5bi 245	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
4	3	con1d 147	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 2988

This theorem is referenced by:  necon2ad  3002  nssne1  3975  nssne2  3976  disjne  4362  nbrne1  5049  nbrne2  5050  peano5  7585  oeeui  8211  domdifsn  8583  ac6sfi  8746  inf3lem2  9076  cnfcom3lem  9150  dfac9  9547  fin23lem21  9750  dedekindle  10793  zneo  12053  modirr  13305  sqrmo  14603  reusq0  14814  pc2dvds  16205  pcadd  16215  oddprmdvds  16229  4sqlem11  16281  latnlej  17670  sylow2blem3  18739  irredn0  19449  irredn1  19452  lssvneln0  19716  lspsnne2  19883  lspfixed  19893  lspindpi  19897  lsmcv  19906  lspsolv  19908  isnzr2  20029  coe1tmmul  20906  dfac14  22223  fbdmn0  22439  filufint  22525  flimfnfcls  22633  alexsubALTlem2  22653  evth  23564  cphsqrtcl2  23791  ovolicc2lem4  24124  lhop1lem  24616  lhop1  24617  lhop2  24618  lhop  24619  deg1add  24704  abelthlem2  25027  logcnlem2  25234  angpined  25416  asinneg  25472  dmgmaddn0  25608  lgsne0  25919  lgsqr  25935  lgsquadlem2  25965  lgsquadlem3  25966  axlowdimlem17  26752  spansncvi  29435  zarcmplem  31234  broutsideof2  33696  unblimceq0lem  33958  poimirlem28  35085  dvasin  35141  dvacos  35142  nninfnub  35189  dvrunz  35392  lsatcvatlem  36345  lkrlsp2  36399  opnlen0  36484  2llnne2N  36704  lnnat  36723  llnn0  36812  lplnn0N  36843  lplnllnneN  36852  llncvrlpln2  36853  llncvrlpln  36854  lvoln0N  36887  lplncvrlvol2  36911  lplncvrlvol  36912  dalempnes  36947  dalemqnet  36948  dalemcea  36956  dalem3  36960  cdlema1N  37087  cdlemb  37090  paddasslem5  37120  llnexchb2lem  37164  osumcllem4N  37255  pexmidlem1N  37266  lhp2lt  37297  lhp2atne  37330  lhp2at0ne  37332  4atexlemunv  37362  4atexlemex2  37367  trlne  37481  trlval4  37484  cdlemc4  37490  cdleme11dN  37558  cdleme11h  37562  cdlemednuN  37596  cdleme20j  37614  cdleme20k  37615  cdleme21at  37624  cdleme35f  37750  cdlemg11b  37938  dia2dimlem1  38360  dihmeetlem3N  38601  dihmeetlem15N  38617  dochsnnz  38746  dochexmidlem1  38756  dochexmidlem7  38762  mapdindp3  39018  fltne  39616  pellexlem1  39770  dfac21  40010  pm13.14  41113  uzlidlring  44553  suppdm  44919