Theorem necon3bd 2976

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1508   ≠ wne 2962

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 199  df-ne 2963

This theorem is referenced by:  necon2ad  2977  nelne1OLD  3060  nelne2OLD  3062  nssne1  3912  nssne2  3913  disjne  4282  nbrne1  4945  nbrne2  4946  peano5  7419  oeeui  8028  domdifsn  8395  ac6sfi  8556  inf3lem2  8885  cnfcom3lem  8959  dfac9  9355  fin23lem21  9558  dedekindle  10603  zneo  11877  modirr  13124  sqrmo  14471  reusq0  14682  pc2dvds  16070  pcadd  16080  oddprmdvds  16094  4sqlem11  16146  latnlej  17549  sylow2blem3  18521  irredn0  19189  irredn1  19192  lssvneln0  19458  lspsnne2  19625  lspfixed  19635  lspindpi  19639  lsmcv  19648  lspsolv  19650  isnzr2  19770  coe1tmmul  20164  dfac14  21946  fbdmn0  22162  filufint  22248  flimfnfcls  22356  alexsubALTlem2  22376  evth  23282  cphsqrtcl2  23509  ovolicc2lem4  23840  lhop1lem  24329  lhop1  24330  lhop2  24331  lhop  24332  deg1add  24416  abelthlem2  24739  logcnlem2  24943  angpined  25125  asinneg  25181  dmgmaddn0  25318  lgsne0  25629  lgsqr  25645  lgsquadlem2  25675  lgsquadlem3  25676  axlowdimlem17  26463  spansncvi  29226  broutsideof2  33137  unblimceq0lem  33398  poimirlem28  34394  dvasin  34452  dvacos  34453  nninfnub  34501  dvrunz  34707  lsatcvatlem  35663  lkrlsp2  35717  opnlen0  35802  2llnne2N  36022  lnnat  36041  llnn0  36130  lplnn0N  36161  lplnllnneN  36170  llncvrlpln2  36171  llncvrlpln  36172  lvoln0N  36205  lplncvrlvol2  36229  lplncvrlvol  36230  dalempnes  36265  dalemqnet  36266  dalemcea  36274  dalem3  36278  cdlema1N  36405  cdlemb  36408  paddasslem5  36438  llnexchb2lem  36482  osumcllem4N  36573  pexmidlem1N  36584  lhp2lt  36615  lhp2atne  36648  lhp2at0ne  36650  4atexlemunv  36680  4atexlemex2  36685  trlne  36799  trlval4  36802  cdlemc4  36808  cdleme11dN  36876  cdleme11h  36880  cdlemednuN  36914  cdleme20j  36932  cdleme20k  36933  cdleme21at  36942  cdleme35f  37068  cdlemg11b  37256  dia2dimlem1  37678  dihmeetlem3N  37919  dihmeetlem15N  37935  dochsnnz  38064  dochexmidlem1  38074  dochexmidlem7  38080  mapdindp3  38336  fltne  38713  pellexlem1  38856  dfac21  39096  pm13.14  40192  uzlidlring  43594  suppdm  43963