Theorem necon3bd 2970

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 2957

This theorem is referenced by:  necon2ad  2971  nssne1  3998  nssne2  3999  disjne  4408  nbrne1  5118  nbrne2  5119  peano5  7870  oeeui  8567  domdifsn  9028  ac6sfi  9224  inf3lem2  9581  cnfcom3lem  9655  dfac9  10090  fin23lem21  10293  1re  11178  dedekindle  11344  zneo  12653  modirr  13952  sqrmo  15261  reusq0  15475  pc2dvds  16898  pcadd  16908  oddprmdvds  16922  4sqlem11  16974  latnlej  18471  sylow2blem3  19645  irredn0  20451  irredn1  20454  isnzr2  20547  lssvneln0  20999  lspsnne2  21168  lspfixed  21178  lspindpi  21182  lsmcv  21191  lspsolv  21193  coe1tmmul  22320  dfac14  23658  fbdmn0  23874  filufint  23960  flimfnfcls  24068  alexsubALTlem2  24088  evth  25001  cphsqrtcl2  25228  ovolicc2lem4  25562  lhop1lem  26055  lhop1  26056  lhop2  26057  lhop  26058  deg1add  26143  abelthlem2  26472  logcnlem2  26685  angpined  26872  asinneg  26928  dmgmaddn0  27064  lgsne0  27376  lgsqr  27392  lgsquadlem2  27422  lgsquadlem3  27423  axlowdimlem17  29105  spansncvi  31801  argcj  32900  constrrecl  34027  zarcmplem  34139  broutsideof2  36436  unblimceq0lem  36908  poimirlem28  38111  dvasin  38167  dvacos  38168  nninfnub  38214  dvrunz  38417  lsatcvatlem  39637  lkrlsp2  39691  opnlen0  39776  2llnne2N  39996  lnnat  40015  llnn0  40104  lplnn0N  40135  lplnllnneN  40144  llncvrlpln2  40145  llncvrlpln  40146  lvoln0N  40179  lplncvrlvol2  40203  lplncvrlvol  40204  dalempnes  40239  dalemqnet  40240  dalemcea  40248  dalem3  40252  cdlema1N  40379  cdlemb  40382  paddasslem5  40412  llnexchb2lem  40456  osumcllem4N  40547  pexmidlem1N  40558  lhp2lt  40589  lhp2atne  40622  lhp2at0ne  40624  4atexlemunv  40654  4atexlemex2  40659  trlne  40773  trlval4  40776  cdlemc4  40782  cdleme11dN  40850  cdleme11h  40854  cdlemednuN  40888  cdleme20j  40906  cdleme20k  40907  cdleme21at  40916  cdleme35f  41042  cdlemg11b  41230  dia2dimlem1  41652  dihmeetlem3N  41893  dihmeetlem15N  41909  dochsnnz  42038  dochexmidlem1  42048  dochexmidlem7  42054  mapdindp3  42310  fltne  43190  pellexlem1  43370  dfac21  43607  pm13.14  44949  uzlidlring  48821  suppdm  49096