Theorem necon3bd 2952

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 2942	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
2		necon3bd.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3	1, 2	biimtrid 241	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
4	3	con1d 145	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2938

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 206  df-ne 2939

This theorem is referenced by:  necon2ad  2953  nssne1  4043  nssne2  4044  disjne  4453  nbrne1  5166  nbrne2  5167  peano5  7886  peano5OLD  7887  oeeui  8604  domdifsn  9056  ac6sfi  9289  inf3lem2  9626  cnfcom3lem  9700  dfac9  10133  fin23lem21  10336  dedekindle  11382  zneo  12649  modirr  13911  sqrmo  15202  reusq0  15413  pc2dvds  16816  pcadd  16826  oddprmdvds  16840  4sqlem11  16892  latnlej  18413  sylow2blem3  19531  irredn0  20314  irredn1  20317  isnzr2  20409  lssvneln0  20706  lspsnne2  20876  lspfixed  20886  lspindpi  20890  lsmcv  20899  lspsolv  20901  coe1tmmul  22019  dfac14  23342  fbdmn0  23558  filufint  23644  flimfnfcls  23752  alexsubALTlem2  23772  evth  24705  cphsqrtcl2  24934  ovolicc2lem4  25269  lhop1lem  25765  lhop1  25766  lhop2  25767  lhop  25768  deg1add  25856  abelthlem2  26180  logcnlem2  26387  angpined  26571  asinneg  26627  dmgmaddn0  26763  lgsne0  27074  lgsqr  27090  lgsquadlem2  27120  lgsquadlem3  27121  axlowdimlem17  28483  spansncvi  31172  zarcmplem  33159  broutsideof2  35398  unblimceq0lem  35685  poimirlem28  36819  dvasin  36875  dvacos  36876  nninfnub  36922  dvrunz  37125  lsatcvatlem  38222  lkrlsp2  38276  opnlen0  38361  2llnne2N  38582  lnnat  38601  llnn0  38690  lplnn0N  38721  lplnllnneN  38730  llncvrlpln2  38731  llncvrlpln  38732  lvoln0N  38765  lplncvrlvol2  38789  lplncvrlvol  38790  dalempnes  38825  dalemqnet  38826  dalemcea  38834  dalem3  38838  cdlema1N  38965  cdlemb  38968  paddasslem5  38998  llnexchb2lem  39042  osumcllem4N  39133  pexmidlem1N  39144  lhp2lt  39175  lhp2atne  39208  lhp2at0ne  39210  4atexlemunv  39240  4atexlemex2  39245  trlne  39359  trlval4  39362  cdlemc4  39368  cdleme11dN  39436  cdleme11h  39440  cdlemednuN  39474  cdleme20j  39492  cdleme20k  39493  cdleme21at  39502  cdleme35f  39628  cdlemg11b  39816  dia2dimlem1  40238  dihmeetlem3N  40479  dihmeetlem15N  40495  dochsnnz  40624  dochexmidlem1  40634  dochexmidlem7  40640  mapdindp3  40896  fltne  41688  pellexlem1  41869  dfac21  42110  pm13.14  43470  uzlidlring  46915  suppdm  47278