Theorem necon3bd 2943

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 2929

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 2930

This theorem is referenced by:  necon2ad  2944  nssne1  4039  nssne2  4040  disjne  4456  nbrne1  5168  nbrne2  5169  peano5  7900  peano5OLD  7901  oeeui  8623  domdifsn  9079  ac6sfi  9312  inf3lem2  9654  cnfcom3lem  9728  dfac9  10161  fin23lem21  10364  dedekindle  11410  zneo  12678  modirr  13943  sqrmo  15234  reusq0  15445  pc2dvds  16851  pcadd  16861  oddprmdvds  16875  4sqlem11  16927  latnlej  18451  sylow2blem3  19589  irredn0  20374  irredn1  20377  isnzr2  20469  lssvneln0  20848  lspsnne2  21018  lspfixed  21028  lspindpi  21032  lsmcv  21041  lspsolv  21043  coe1tmmul  22221  dfac14  23566  fbdmn0  23782  filufint  23868  flimfnfcls  23976  alexsubALTlem2  23996  evth  24929  cphsqrtcl2  25158  ovolicc2lem4  25493  lhop1lem  25990  lhop1  25991  lhop2  25992  lhop  25993  deg1add  26083  abelthlem2  26414  logcnlem2  26622  angpined  26807  asinneg  26863  dmgmaddn0  27000  lgsne0  27313  lgsqr  27329  lgsquadlem2  27359  lgsquadlem3  27360  axlowdimlem17  28841  spansncvi  31534  zarcmplem  33610  broutsideof2  35846  unblimceq0lem  36109  poimirlem28  37249  dvasin  37305  dvacos  37306  nninfnub  37352  dvrunz  37555  lsatcvatlem  38648  lkrlsp2  38702  opnlen0  38787  2llnne2N  39008  lnnat  39027  llnn0  39116  lplnn0N  39147  lplnllnneN  39156  llncvrlpln2  39157  llncvrlpln  39158  lvoln0N  39191  lplncvrlvol2  39215  lplncvrlvol  39216  dalempnes  39251  dalemqnet  39252  dalemcea  39260  dalem3  39264  cdlema1N  39391  cdlemb  39394  paddasslem5  39424  llnexchb2lem  39468  osumcllem4N  39559  pexmidlem1N  39570  lhp2lt  39601  lhp2atne  39634  lhp2at0ne  39636  4atexlemunv  39666  4atexlemex2  39671  trlne  39785  trlval4  39788  cdlemc4  39794  cdleme11dN  39862  cdleme11h  39866  cdlemednuN  39900  cdleme20j  39918  cdleme20k  39919  cdleme21at  39928  cdleme35f  40054  cdlemg11b  40242  dia2dimlem1  40664  dihmeetlem3N  40905  dihmeetlem15N  40921  dochsnnz  41050  dochexmidlem1  41060  dochexmidlem7  41066  mapdindp3  41322  fltne  42200  pellexlem1  42388  dfac21  42629  pm13.14  43985  uzlidlring  47480  suppdm  47761