Theorem necon3bd 2947

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  necon2ad  2948  nssne1  3998  nssne2  3999  disjne  4409  nbrne1  5119  nbrne2  5120  peano5  7845  oeeui  8540  domdifsn  9000  ac6sfi  9196  inf3lem2  9550  cnfcom3lem  9624  dfac9  10059  fin23lem21  10261  1re  11144  dedekindle  11309  zneo  12587  modirr  13877  sqrmo  15186  reusq0  15400  pc2dvds  16819  pcadd  16829  oddprmdvds  16843  4sqlem11  16895  latnlej  18391  sylow2blem3  19563  irredn0  20371  irredn1  20374  isnzr2  20463  lssvneln0  20915  lspsnne2  21085  lspfixed  21095  lspindpi  21099  lsmcv  21108  lspsolv  21110  coe1tmmul  22231  dfac14  23574  fbdmn0  23790  filufint  23876  flimfnfcls  23984  alexsubALTlem2  24004  evth  24926  cphsqrtcl2  25154  ovolicc2lem4  25489  lhop1lem  25986  lhop1  25987  lhop2  25988  lhop  25989  deg1add  26076  abelthlem2  26410  logcnlem2  26620  angpined  26808  asinneg  26864  dmgmaddn0  27001  lgsne0  27314  lgsqr  27330  lgsquadlem2  27360  lgsquadlem3  27361  axlowdimlem17  29043  spansncvi  31739  argcj  32838  constrrecl  33946  zarcmplem  34058  broutsideof2  36335  unblimceq0lem  36725  poimirlem28  37896  dvasin  37952  dvacos  37953  nninfnub  37999  dvrunz  38202  lsatcvatlem  39422  lkrlsp2  39476  opnlen0  39561  2llnne2N  39781  lnnat  39800  llnn0  39889  lplnn0N  39920  lplnllnneN  39929  llncvrlpln2  39930  llncvrlpln  39931  lvoln0N  39964  lplncvrlvol2  39988  lplncvrlvol  39989  dalempnes  40024  dalemqnet  40025  dalemcea  40033  dalem3  40037  cdlema1N  40164  cdlemb  40167  paddasslem5  40197  llnexchb2lem  40241  osumcllem4N  40332  pexmidlem1N  40343  lhp2lt  40374  lhp2atne  40407  lhp2at0ne  40409  4atexlemunv  40439  4atexlemex2  40444  trlne  40558  trlval4  40561  cdlemc4  40567  cdleme11dN  40635  cdleme11h  40639  cdlemednuN  40673  cdleme20j  40691  cdleme20k  40692  cdleme21at  40701  cdleme35f  40827  cdlemg11b  41015  dia2dimlem1  41437  dihmeetlem3N  41678  dihmeetlem15N  41694  dochsnnz  41823  dochexmidlem1  41833  dochexmidlem7  41839  mapdindp3  42095  fltne  42999  pellexlem1  43183  dfac21  43420  pm13.14  44762  uzlidlring  48592  suppdm  48867