Theorem necon3bd 2951

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  necon2ad  2952  nssne1  4057  nssne2  4058  disjne  4460  nbrne1  5166  nbrne2  5167  peano5  7915  oeeui  8638  domdifsn  9092  ac6sfi  9317  inf3lem2  9666  cnfcom3lem  9740  dfac9  10174  fin23lem21  10376  dedekindle  11422  zneo  12698  modirr  13979  sqrmo  15286  reusq0  15497  pc2dvds  16912  pcadd  16922  oddprmdvds  16936  4sqlem11  16988  latnlej  18513  sylow2blem3  19654  irredn0  20439  irredn1  20442  isnzr2  20534  lssvneln0  20967  lspsnne2  21137  lspfixed  21147  lspindpi  21151  lsmcv  21160  lspsolv  21162  coe1tmmul  22295  dfac14  23641  fbdmn0  23857  filufint  23943  flimfnfcls  24051  alexsubALTlem2  24071  evth  25004  cphsqrtcl2  25233  ovolicc2lem4  25568  lhop1lem  26066  lhop1  26067  lhop2  26068  lhop  26069  deg1add  26156  abelthlem2  26490  logcnlem2  26699  angpined  26887  asinneg  26943  dmgmaddn0  27080  lgsne0  27393  lgsqr  27409  lgsquadlem2  27439  lgsquadlem3  27440  axlowdimlem17  28987  spansncvi  31680  zarcmplem  33841  broutsideof2  36103  unblimceq0lem  36488  poimirlem28  37634  dvasin  37690  dvacos  37691  nninfnub  37737  dvrunz  37940  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  42630  pellexlem1  42816  dfac21  43054  pm13.14  44404  uzlidlring  48078  suppdm  48355