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  4009  nssne2  4010  disjne  4418  nbrne1  5126  nbrne2  5127  peano5  7869  oeeui  8566  domdifsn  9024  ac6sfi  9231  inf3lem2  9582  cnfcom3lem  9656  dfac9  10090  fin23lem21  10292  1re  11174  dedekindle  11338  zneo  12617  modirr  13907  sqrmo  15217  reusq0  15431  pc2dvds  16850  pcadd  16860  oddprmdvds  16874  4sqlem11  16926  latnlej  18415  sylow2blem3  19552  irredn0  20332  irredn1  20335  isnzr2  20427  lssvneln0  20858  lspsnne2  21028  lspfixed  21038  lspindpi  21042  lsmcv  21051  lspsolv  21053  coe1tmmul  22163  dfac14  23505  fbdmn0  23721  filufint  23807  flimfnfcls  23915  alexsubALTlem2  23935  evth  24858  cphsqrtcl2  25086  ovolicc2lem4  25421  lhop1lem  25918  lhop1  25919  lhop2  25920  lhop  25921  deg1add  26008  abelthlem2  26342  logcnlem2  26552  angpined  26740  asinneg  26796  dmgmaddn0  26933  lgsne0  27246  lgsqr  27262  lgsquadlem2  27292  lgsquadlem3  27293  axlowdimlem17  28885  spansncvi  31581  argcj  32672  constrrecl  33759  zarcmplem  33871  broutsideof2  36110  unblimceq0lem  36494  poimirlem28  37642  dvasin  37698  dvacos  37699  nninfnub  37745  dvrunz  37948  lsatcvatlem  39042  lkrlsp2  39096  opnlen0  39181  2llnne2N  39402  lnnat  39421  llnn0  39510  lplnn0N  39541  lplnllnneN  39550  llncvrlpln2  39551  llncvrlpln  39552  lvoln0N  39585  lplncvrlvol2  39609  lplncvrlvol  39610  dalempnes  39645  dalemqnet  39646  dalemcea  39654  dalem3  39658  cdlema1N  39785  cdlemb  39788  paddasslem5  39818  llnexchb2lem  39862  osumcllem4N  39953  pexmidlem1N  39964  lhp2lt  39995  lhp2atne  40028  lhp2at0ne  40030  4atexlemunv  40060  4atexlemex2  40065  trlne  40179  trlval4  40182  cdlemc4  40188  cdleme11dN  40256  cdleme11h  40260  cdlemednuN  40294  cdleme20j  40312  cdleme20k  40313  cdleme21at  40322  cdleme35f  40448  cdlemg11b  40636  dia2dimlem1  41058  dihmeetlem3N  41299  dihmeetlem15N  41315  dochsnnz  41444  dochexmidlem1  41454  dochexmidlem7  41460  mapdindp3  41716  fltne  42632  pellexlem1  42817  dfac21  43055  pm13.14  44398  uzlidlring  48223  suppdm  48499