Theorem necon3bd 2837

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 2827	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
2		necon3bd.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3	1, 2	syl5bi 232	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
4	3	con1d 139	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  necon2ad  2838  nelne1  2919  nelne2  2920  nssne1  3694  nssne2  3695  disjne  4055  nbrne1  4704  nbrne2  4705  peano5  7131  oeeui  7727  domdifsn  8084  ac6sfi  8245  inf3lem2  8564  cnfcom3lem  8638  dfac9  8996  fin23lem21  9199  dedekindle  10239  zneo  11498  modirr  12781  sqrmo  14036  pc2dvds  15630  pcadd  15640  oddprmdvds  15654  4sqlem11  15706  latnlej  17115  sylow2blem3  18083  irredn0  18749  irredn1  18752  lssneln0  19000  lspsnne2  19166  lspfixed  19176  lspindpi  19180  lsmcv  19189  lspsolv  19191  isnzr2  19311  coe1tmmul  19695  dfac14  21469  fbdmn0  21685  filufint  21771  flimfnfcls  21879  alexsubALTlem2  21899  evth  22805  cphsqrtcl2  23032  ovolicc2lem4  23334  lhop1lem  23821  lhop1  23822  lhop2  23823  lhop  23824  deg1add  23908  abelthlem2  24231  logcnlem2  24434  angpined  24602  asinneg  24658  dmgmaddn0  24794  lgsne0  25105  lgsqr  25121  lgsquadlem2  25151  lgsquadlem3  25152  axlowdimlem17  25883  spansncvi  28639  broutsideof2  32354  unblimceq0lem  32622  poimirlem28  33567  dvasin  33626  dvacos  33627  nninfnub  33677  dvrunz  33883  lsatcvatlem  34654  lkrlsp2  34708  opnlen0  34793  2llnne2N  35012  lnnat  35031  llnn0  35120  lplnn0N  35151  lplnllnneN  35160  llncvrlpln2  35161  llncvrlpln  35162  lvoln0N  35195  lplncvrlvol2  35219  lplncvrlvol  35220  dalempnes  35255  dalemqnet  35256  dalemcea  35264  dalem3  35268  cdlema1N  35395  cdlemb  35398  paddasslem5  35428  llnexchb2lem  35472  osumcllem4N  35563  pexmidlem1N  35574  lhp2lt  35605  lhp2atne  35638  lhp2at0ne  35640  4atexlemunv  35670  4atexlemex2  35675  trlne  35790  trlval4  35793  cdlemc4  35799  cdleme11dN  35867  cdleme11h  35871  cdlemednuN  35905  cdleme20j  35923  cdleme20k  35924  cdleme21at  35933  cdleme35f  36059  cdlemg11b  36247  dia2dimlem1  36670  dihmeetlem3N  36911  dihmeetlem15N  36927  dochsnnz  37056  dochexmidlem1  37066  dochexmidlem7  37072  mapdindp3  37328  pellexlem1  37710  dfac21  37953  pm13.14  38927  uzlidlring  42254  suppdm  42625