Theorem necon3bd 3030

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  necon2ad  3031  nelne1OLD  3114  nelne2OLD  3116  nssne1  4027  nssne2  4028  disjne  4404  nbrne1  5085  nbrne2  5086  peano5  7605  oeeui  8228  domdifsn  8600  ac6sfi  8762  inf3lem2  9092  cnfcom3lem  9166  dfac9  9562  fin23lem21  9761  dedekindle  10804  zneo  12066  modirr  13311  sqrmo  14611  reusq0  14822  pc2dvds  16215  pcadd  16225  oddprmdvds  16239  4sqlem11  16291  latnlej  17678  sylow2blem3  18747  irredn0  19453  irredn1  19456  lssvneln0  19723  lspsnne2  19890  lspfixed  19900  lspindpi  19904  lsmcv  19913  lspsolv  19915  isnzr2  20036  coe1tmmul  20445  dfac14  22226  fbdmn0  22442  filufint  22528  flimfnfcls  22636  alexsubALTlem2  22656  evth  23563  cphsqrtcl2  23790  ovolicc2lem4  24121  lhop1lem  24610  lhop1  24611  lhop2  24612  lhop  24613  deg1add  24697  abelthlem2  25020  logcnlem2  25226  angpined  25408  asinneg  25464  dmgmaddn0  25600  lgsne0  25911  lgsqr  25927  lgsquadlem2  25957  lgsquadlem3  25958  axlowdimlem17  26744  spansncvi  29429  broutsideof2  33583  unblimceq0lem  33845  poimirlem28  34935  dvasin  34993  dvacos  34994  nninfnub  35041  dvrunz  35247  lsatcvatlem  36200  lkrlsp2  36254  opnlen0  36339  2llnne2N  36559  lnnat  36578  llnn0  36667  lplnn0N  36698  lplnllnneN  36707  llncvrlpln2  36708  llncvrlpln  36709  lvoln0N  36742  lplncvrlvol2  36766  lplncvrlvol  36767  dalempnes  36802  dalemqnet  36803  dalemcea  36811  dalem3  36815  cdlema1N  36942  cdlemb  36945  paddasslem5  36975  llnexchb2lem  37019  osumcllem4N  37110  pexmidlem1N  37121  lhp2lt  37152  lhp2atne  37185  lhp2at0ne  37187  4atexlemunv  37217  4atexlemex2  37222  trlne  37336  trlval4  37339  cdlemc4  37345  cdleme11dN  37413  cdleme11h  37417  cdlemednuN  37451  cdleme20j  37469  cdleme20k  37470  cdleme21at  37479  cdleme35f  37605  cdlemg11b  37793  dia2dimlem1  38215  dihmeetlem3N  38456  dihmeetlem15N  38472  dochsnnz  38601  dochexmidlem1  38611  dochexmidlem7  38617  mapdindp3  38873  fltne  39292  pellexlem1  39446  dfac21  39686  pm13.14  40761  uzlidlring  44220  suppdm  44585