Theorem necon3bd 2957

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

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

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 2944

This theorem is referenced by:  necon2ad  2958  nssne1  3981  nssne2  3982  disjne  4388  nbrne1  5093  nbrne2  5094  peano5  7740  peano5OLD  7741  oeeui  8433  domdifsn  8841  ac6sfi  9058  inf3lem2  9387  cnfcom3lem  9461  dfac9  9892  fin23lem21  10095  dedekindle  11139  zneo  12403  modirr  13662  sqrmo  14963  reusq0  15174  pc2dvds  16580  pcadd  16590  oddprmdvds  16604  4sqlem11  16656  latnlej  18174  sylow2blem3  19227  irredn0  19945  irredn1  19948  lssvneln0  20213  lspsnne2  20380  lspfixed  20390  lspindpi  20394  lsmcv  20403  lspsolv  20405  isnzr2  20534  coe1tmmul  21448  dfac14  22769  fbdmn0  22985  filufint  23071  flimfnfcls  23179  alexsubALTlem2  23199  evth  24122  cphsqrtcl2  24350  ovolicc2lem4  24684  lhop1lem  25177  lhop1  25178  lhop2  25179  lhop  25180  deg1add  25268  abelthlem2  25591  logcnlem2  25798  angpined  25980  asinneg  26036  dmgmaddn0  26172  lgsne0  26483  lgsqr  26499  lgsquadlem2  26529  lgsquadlem3  26530  axlowdimlem17  27326  spansncvi  30014  zarcmplem  31831  broutsideof2  34424  unblimceq0lem  34686  poimirlem28  35805  dvasin  35861  dvacos  35862  nninfnub  35909  dvrunz  36112  lsatcvatlem  37063  lkrlsp2  37117  opnlen0  37202  2llnne2N  37422  lnnat  37441  llnn0  37530  lplnn0N  37561  lplnllnneN  37570  llncvrlpln2  37571  llncvrlpln  37572  lvoln0N  37605  lplncvrlvol2  37629  lplncvrlvol  37630  dalempnes  37665  dalemqnet  37666  dalemcea  37674  dalem3  37678  cdlema1N  37805  cdlemb  37808  paddasslem5  37838  llnexchb2lem  37882  osumcllem4N  37973  pexmidlem1N  37984  lhp2lt  38015  lhp2atne  38048  lhp2at0ne  38050  4atexlemunv  38080  4atexlemex2  38085  trlne  38199  trlval4  38202  cdlemc4  38208  cdleme11dN  38276  cdleme11h  38280  cdlemednuN  38314  cdleme20j  38332  cdleme20k  38333  cdleme21at  38342  cdleme35f  38468  cdlemg11b  38656  dia2dimlem1  39078  dihmeetlem3N  39319  dihmeetlem15N  39335  dochsnnz  39464  dochexmidlem1  39474  dochexmidlem7  39480  mapdindp3  39736  fltne  40481  pellexlem1  40651  dfac21  40891  pm13.14  42027  uzlidlring  45487  suppdm  45851