Theorem necon3bd 2946

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  necon2ad  2947  nssne1  3984  nssne2  3985  disjne  4395  nbrne1  5104  nbrne2  5105  peano5  7844  oeeui  8538  domdifsn  8998  ac6sfi  9194  inf3lem2  9550  cnfcom3lem  9624  dfac9  10059  fin23lem21  10261  1re  11144  dedekindle  11310  zneo  12612  modirr  13904  sqrmo  15213  reusq0  15427  pc2dvds  16850  pcadd  16860  oddprmdvds  16874  4sqlem11  16926  latnlej  18422  sylow2blem3  19597  irredn0  20403  irredn1  20406  isnzr2  20495  lssvneln0  20947  lspsnne2  21116  lspfixed  21126  lspindpi  21130  lsmcv  21139  lspsolv  21141  coe1tmmul  22242  dfac14  23583  fbdmn0  23799  filufint  23885  flimfnfcls  23993  alexsubALTlem2  24013  evth  24926  cphsqrtcl2  25153  ovolicc2lem4  25487  lhop1lem  25980  lhop1  25981  lhop2  25982  lhop  25983  deg1add  26068  abelthlem2  26397  logcnlem2  26607  angpined  26794  asinneg  26850  dmgmaddn0  26986  lgsne0  27298  lgsqr  27314  lgsquadlem2  27344  lgsquadlem3  27345  axlowdimlem17  29027  spansncvi  31723  argcj  32821  constrrecl  33913  zarcmplem  34025  broutsideof2  36304  unblimceq0lem  36766  poimirlem28  37969  dvasin  38025  dvacos  38026  nninfnub  38072  dvrunz  38275  lsatcvatlem  39495  lkrlsp2  39549  opnlen0  39634  2llnne2N  39854  lnnat  39873  llnn0  39962  lplnn0N  39993  lplnllnneN  40002  llncvrlpln2  40003  llncvrlpln  40004  lvoln0N  40037  lplncvrlvol2  40061  lplncvrlvol  40062  dalempnes  40097  dalemqnet  40098  dalemcea  40106  dalem3  40110  cdlema1N  40237  cdlemb  40240  paddasslem5  40270  llnexchb2lem  40314  osumcllem4N  40405  pexmidlem1N  40416  lhp2lt  40447  lhp2atne  40480  lhp2at0ne  40482  4atexlemunv  40512  4atexlemex2  40517  trlne  40631  trlval4  40634  cdlemc4  40640  cdleme11dN  40708  cdleme11h  40712  cdlemednuN  40746  cdleme20j  40764  cdleme20k  40765  cdleme21at  40774  cdleme35f  40900  cdlemg11b  41088  dia2dimlem1  41510  dihmeetlem3N  41751  dihmeetlem15N  41767  dochsnnz  41896  dochexmidlem1  41906  dochexmidlem7  41912  mapdindp3  42168  fltne  43077  pellexlem1  43257  dfac21  43494  pm13.14  44836  uzlidlring  48711  suppdm  48986