Theorem necon3bd 2975

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2962

This theorem is used by:  necon2ad  2976  nssne1  4002  nssne2  4003  disjne  4418  nbrne1  5135  nbrne2  5136  peano5  7899  oeeui  8597  domdifsn  9058  ac6sfi  9254  inf3lem2  9608  cnfcom3lem  9682  dfac9  10139  fin23lem21  10341  1re  11226  dedekindle  11392  zneo  12697  modirr  13998  sqrmo  15328  reusq0  15542  pc2dvds  16964  pcadd  16974  oddprmdvds  16988  4sqlem11  17040  latnlej  18537  sylow2blem3  19723  irredn0  20538  irredn1  20541  isnzr2  20652  lssvneln0  21110  lspsnne2  21279  lspfixed  21289  lspindpi  21293  lsmcv  21302  lspsolv  21304  coe1tmmul  22475  dfac14  23812  fbdmn0  24028  filufint  24114  flimfnfcls  24222  alexsubALTlem2  24242  evth  25155  cphsqrtcl2  25382  ovolicc2lem4  25716  lhop1lem  26209  lhop1  26210  lhop2  26211  lhop  26212  deg1add  26297  abelthlem2  26632  logcnlem2  26845  angpined  27032  asinneg  27088  dmgmaddn0  27224  lgsne0  27536  lgsqr  27552  lgsquadlem2  27582  lgsquadlem3  27583  axlowdimlem17  29345  spansncvi  32041  argcj  33130  constrrecl  34190  zarcmplem  34302  nelscottrankgt  35543  broutsideof2  36635  unblimceq0lem  37136  poimirlem28  38340  dvasin  38396  dvacos  38397  nninfnub  38443  dvrunz  38646  lsatcvatlem  39864  lkrlsp2  39918  opnlen0  40003  2llnne2N  40223  lnnat  40242  llnn0  40331  lplnn0N  40362  lplnllnneN  40371  llncvrlpln2  40372  llncvrlpln  40373  lvoln0N  40406  lplncvrlvol2  40430  lplncvrlvol  40431  dalempnes  40466  dalemqnet  40467  dalemcea  40475  dalem3  40479  cdlema1N  40606  cdlemb  40609  paddasslem5  40639  llnexchb2lem  40683  osumcllem4N  40774  pexmidlem1N  40785  lhp2lt  40816  lhp2atne  40849  lhp2at0ne  40851  4atexlemunv  40881  4atexlemex2  40886  trlne  41000  trlval4  41003  cdlemc4  41009  cdleme11dN  41077  cdleme11h  41081  cdlemednuN  41115  cdleme20j  41133  cdleme20k  41134  cdleme21at  41143  cdleme35f  41269  cdlemg11b  41457  dia2dimlem1  41879  dihmeetlem3N  42120  dihmeetlem15N  42136  dochsnnz  42265  dochexmidlem1  42275  dochexmidlem7  42281  mapdindp3  42537  fltne  43417  pellexlem1  43597  dfac21  43834  pm13.14  45160  uzlidlring  49041  suppdm  49331