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  3982  nssne2  3983  disjne  4390  nbrne1  5094  nbrne2  5095  peano5  7732  peano5OLD  7733  oeeui  8422  domdifsn  8830  ac6sfi  9047  inf3lem2  9376  cnfcom3lem  9450  dfac9  9881  fin23lem21  10084  dedekindle  11128  zneo  12392  modirr  13651  sqrmo  14952  reusq0  15163  pc2dvds  16569  pcadd  16579  oddprmdvds  16593  4sqlem11  16645  latnlej  18163  sylow2blem3  19216  irredn0  19934  irredn1  19937  lssvneln0  20202  lspsnne2  20369  lspfixed  20379  lspindpi  20383  lsmcv  20392  lspsolv  20394  isnzr2  20523  coe1tmmul  21437  dfac14  22758  fbdmn0  22974  filufint  23060  flimfnfcls  23168  alexsubALTlem2  23188  evth  24111  cphsqrtcl2  24339  ovolicc2lem4  24673  lhop1lem  25166  lhop1  25167  lhop2  25168  lhop  25169  deg1add  25257  abelthlem2  25580  logcnlem2  25787  angpined  25969  asinneg  26025  dmgmaddn0  26161  lgsne0  26472  lgsqr  26488  lgsquadlem2  26518  lgsquadlem3  26519  axlowdimlem17  27315  spansncvi  30001  zarcmplem  31818  broutsideof2  34411  unblimceq0lem  34673  poimirlem28  35792  dvasin  35848  dvacos  35849  nninfnub  35896  dvrunz  36099  lsatcvatlem  37050  lkrlsp2  37104  opnlen0  37189  2llnne2N  37409  lnnat  37428  llnn0  37517  lplnn0N  37548  lplnllnneN  37557  llncvrlpln2  37558  llncvrlpln  37559  lvoln0N  37592  lplncvrlvol2  37616  lplncvrlvol  37617  dalempnes  37652  dalemqnet  37653  dalemcea  37661  dalem3  37665  cdlema1N  37792  cdlemb  37795  paddasslem5  37825  llnexchb2lem  37869  osumcllem4N  37960  pexmidlem1N  37971  lhp2lt  38002  lhp2atne  38035  lhp2at0ne  38037  4atexlemunv  38067  4atexlemex2  38072  trlne  38186  trlval4  38189  cdlemc4  38195  cdleme11dN  38263  cdleme11h  38267  cdlemednuN  38301  cdleme20j  38319  cdleme20k  38320  cdleme21at  38329  cdleme35f  38455  cdlemg11b  38643  dia2dimlem1  39065  dihmeetlem3N  39306  dihmeetlem15N  39322  dochsnnz  39451  dochexmidlem1  39461  dochexmidlem7  39467  mapdindp3  39723  fltne  40468  pellexlem1  40638  dfac21  40878  pm13.14  41987  uzlidlring  45444  suppdm  45808