Theorem necon3bd 2939

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon2ad  2940  nssne1  4000  nssne2  4001  disjne  4408  nbrne1  5114  nbrne2  5115  peano5  7833  oeeui  8527  domdifsn  8984  ac6sfi  9189  inf3lem2  9544  cnfcom3lem  9618  dfac9  10050  fin23lem21  10252  1re  11134  dedekindle  11298  zneo  12577  modirr  13867  sqrmo  15176  reusq0  15390  pc2dvds  16809  pcadd  16819  oddprmdvds  16833  4sqlem11  16885  latnlej  18380  sylow2blem3  19519  irredn0  20326  irredn1  20329  isnzr2  20421  lssvneln0  20873  lspsnne2  21043  lspfixed  21053  lspindpi  21057  lsmcv  21066  lspsolv  21068  coe1tmmul  22179  dfac14  23521  fbdmn0  23737  filufint  23823  flimfnfcls  23931  alexsubALTlem2  23951  evth  24874  cphsqrtcl2  25102  ovolicc2lem4  25437  lhop1lem  25934  lhop1  25935  lhop2  25936  lhop  25937  deg1add  26024  abelthlem2  26358  logcnlem2  26568  angpined  26756  asinneg  26812  dmgmaddn0  26949  lgsne0  27262  lgsqr  27278  lgsquadlem2  27308  lgsquadlem3  27309  axlowdimlem17  28921  spansncvi  31614  argcj  32705  constrrecl  33738  zarcmplem  33850  broutsideof2  36098  unblimceq0lem  36482  poimirlem28  37630  dvasin  37686  dvacos  37687  nninfnub  37733  dvrunz  37936  lsatcvatlem  39030  lkrlsp2  39084  opnlen0  39169  2llnne2N  39390  lnnat  39409  llnn0  39498  lplnn0N  39529  lplnllnneN  39538  llncvrlpln2  39539  llncvrlpln  39540  lvoln0N  39573  lplncvrlvol2  39597  lplncvrlvol  39598  dalempnes  39633  dalemqnet  39634  dalemcea  39642  dalem3  39646  cdlema1N  39773  cdlemb  39776  paddasslem5  39806  llnexchb2lem  39850  osumcllem4N  39941  pexmidlem1N  39952  lhp2lt  39983  lhp2atne  40016  lhp2at0ne  40018  4atexlemunv  40048  4atexlemex2  40053  trlne  40167  trlval4  40170  cdlemc4  40176  cdleme11dN  40244  cdleme11h  40248  cdlemednuN  40282  cdleme20j  40300  cdleme20k  40301  cdleme21at  40310  cdleme35f  40436  cdlemg11b  40624  dia2dimlem1  41046  dihmeetlem3N  41287  dihmeetlem15N  41303  dochsnnz  41432  dochexmidlem1  41442  dochexmidlem7  41448  mapdindp3  41704  fltne  42620  pellexlem1  42805  dfac21  43042  pm13.14  44385  uzlidlring  48223  suppdm  48499