Theorem necon3bd 2953

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2939

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 2940

This theorem is referenced by:  necon2ad  2954  nssne1  4009  nssne2  4010  disjne  4419  nbrne1  5129  nbrne2  5130  peano5  7835  peano5OLD  7836  oeeui  8554  domdifsn  9005  ac6sfi  9238  inf3lem2  9574  cnfcom3lem  9648  dfac9  10081  fin23lem21  10284  dedekindle  11328  zneo  12595  modirr  13857  sqrmo  15148  reusq0  15359  pc2dvds  16762  pcadd  16772  oddprmdvds  16786  4sqlem11  16838  latnlej  18359  sylow2blem3  19418  irredn0  20148  irredn1  20151  isnzr2  20207  lssvneln0  20469  lspsnne2  20638  lspfixed  20648  lspindpi  20652  lsmcv  20661  lspsolv  20663  coe1tmmul  21685  dfac14  23006  fbdmn0  23222  filufint  23308  flimfnfcls  23416  alexsubALTlem2  23436  evth  24359  cphsqrtcl2  24587  ovolicc2lem4  24921  lhop1lem  25414  lhop1  25415  lhop2  25416  lhop  25417  deg1add  25505  abelthlem2  25828  logcnlem2  26035  angpined  26217  asinneg  26273  dmgmaddn0  26409  lgsne0  26720  lgsqr  26736  lgsquadlem2  26766  lgsquadlem3  26767  axlowdimlem17  27970  spansncvi  30657  zarcmplem  32551  broutsideof2  34783  unblimceq0lem  35045  poimirlem28  36179  dvasin  36235  dvacos  36236  nninfnub  36283  dvrunz  36486  lsatcvatlem  37584  lkrlsp2  37638  opnlen0  37723  2llnne2N  37944  lnnat  37963  llnn0  38052  lplnn0N  38083  lplnllnneN  38092  llncvrlpln2  38093  llncvrlpln  38094  lvoln0N  38127  lplncvrlvol2  38151  lplncvrlvol  38152  dalempnes  38187  dalemqnet  38188  dalemcea  38196  dalem3  38200  cdlema1N  38327  cdlemb  38330  paddasslem5  38360  llnexchb2lem  38404  osumcllem4N  38495  pexmidlem1N  38506  lhp2lt  38537  lhp2atne  38570  lhp2at0ne  38572  4atexlemunv  38602  4atexlemex2  38607  trlne  38721  trlval4  38724  cdlemc4  38730  cdleme11dN  38798  cdleme11h  38802  cdlemednuN  38836  cdleme20j  38854  cdleme20k  38855  cdleme21at  38864  cdleme35f  38990  cdlemg11b  39178  dia2dimlem1  39600  dihmeetlem3N  39841  dihmeetlem15N  39857  dochsnnz  39986  dochexmidlem1  39996  dochexmidlem7  40002  mapdindp3  40258  fltne  41040  pellexlem1  41210  dfac21  41451  pm13.14  42811  uzlidlring  46347  suppdm  46711