Theorem necon3bd 2972

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  necon2ad  2973  nssne1  4000  nssne2  4001  disjne  4416  nbrne1  5131  nbrne2  5132  peano5  7891  oeeui  8589  domdifsn  9049  ac6sfi  9245  inf3lem2  9599  cnfcom3lem  9673  dfac9  10121  fin23lem21  10324  1re  11209  dedekindle  11375  zneo  12680  modirr  13980  sqrmo  15304  reusq0  15518  pc2dvds  16940  pcadd  16950  oddprmdvds  16964  4sqlem11  17016  latnlej  18513  sylow2blem3  19693  irredn0  20506  irredn1  20509  isnzr2  20602  lssvneln0  21054  lspsnne2  21223  lspfixed  21233  lspindpi  21237  lsmcv  21246  lspsolv  21248  coe1tmmul  22419  dfac14  23756  fbdmn0  23972  filufint  24058  flimfnfcls  24166  alexsubALTlem2  24186  evth  25099  cphsqrtcl2  25326  ovolicc2lem4  25660  lhop1lem  26153  lhop1  26154  lhop2  26155  lhop  26156  deg1add  26241  abelthlem2  26573  logcnlem2  26786  angpined  26973  asinneg  27029  dmgmaddn0  27165  lgsne0  27477  lgsqr  27493  lgsquadlem2  27523  lgsquadlem3  27524  axlowdimlem17  29286  spansncvi  31982  argcj  33071  constrrecl  34137  zarcmplem  34249  nelscottrankgt  35496  broutsideof2  36592  unblimceq0lem  37073  poimirlem28  38277  dvasin  38333  dvacos  38334  nninfnub  38380  dvrunz  38583  lsatcvatlem  39801  lkrlsp2  39855  opnlen0  39940  2llnne2N  40160  lnnat  40179  llnn0  40268  lplnn0N  40299  lplnllnneN  40308  llncvrlpln2  40309  llncvrlpln  40310  lvoln0N  40343  lplncvrlvol2  40367  lplncvrlvol  40368  dalempnes  40403  dalemqnet  40404  dalemcea  40412  dalem3  40416  cdlema1N  40543  cdlemb  40546  paddasslem5  40576  llnexchb2lem  40620  osumcllem4N  40711  pexmidlem1N  40722  lhp2lt  40753  lhp2atne  40786  lhp2at0ne  40788  4atexlemunv  40818  4atexlemex2  40823  trlne  40937  trlval4  40940  cdlemc4  40946  cdleme11dN  41014  cdleme11h  41018  cdlemednuN  41052  cdleme20j  41070  cdleme20k  41071  cdleme21at  41080  cdleme35f  41206  cdlemg11b  41394  dia2dimlem1  41816  dihmeetlem3N  42057  dihmeetlem15N  42073  dochsnnz  42202  dochexmidlem1  42212  dochexmidlem7  42218  mapdindp3  42474  fltne  43356  pellexlem1  43536  dfac21  43773  pm13.14  45099  uzlidlring  48977  suppdm  49267