Theorem necon3bd 2939

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon2ad  2940  nssne1  3998  nssne2  3999  disjne  4406  nbrne1  5111  nbrne2  5112  peano5  7826  oeeui  8520  domdifsn  8977  ac6sfi  9173  inf3lem2  9525  cnfcom3lem  9599  dfac9  10031  fin23lem21  10233  1re  11115  dedekindle  11280  zneo  12559  modirr  13849  sqrmo  15158  reusq0  15372  pc2dvds  16791  pcadd  16801  oddprmdvds  16815  4sqlem11  16867  latnlej  18362  sylow2blem3  19501  irredn0  20308  irredn1  20311  isnzr2  20403  lssvneln0  20855  lspsnne2  21025  lspfixed  21035  lspindpi  21039  lsmcv  21048  lspsolv  21050  coe1tmmul  22161  dfac14  23503  fbdmn0  23719  filufint  23805  flimfnfcls  23913  alexsubALTlem2  23933  evth  24856  cphsqrtcl2  25084  ovolicc2lem4  25419  lhop1lem  25916  lhop1  25917  lhop2  25918  lhop  25919  deg1add  26006  abelthlem2  26340  logcnlem2  26550  angpined  26738  asinneg  26794  dmgmaddn0  26931  lgsne0  27244  lgsqr  27260  lgsquadlem2  27290  lgsquadlem3  27291  axlowdimlem17  28903  spansncvi  31596  argcj  32692  constrrecl  33736  zarcmplem  33848  broutsideof2  36096  unblimceq0lem  36480  poimirlem28  37628  dvasin  37684  dvacos  37685  nninfnub  37731  dvrunz  37934  lsatcvatlem  39028  lkrlsp2  39082  opnlen0  39167  2llnne2N  39387  lnnat  39406  llnn0  39495  lplnn0N  39526  lplnllnneN  39535  llncvrlpln2  39536  llncvrlpln  39537  lvoln0N  39570  lplncvrlvol2  39594  lplncvrlvol  39595  dalempnes  39630  dalemqnet  39631  dalemcea  39639  dalem3  39643  cdlema1N  39770  cdlemb  39773  paddasslem5  39803  llnexchb2lem  39847  osumcllem4N  39938  pexmidlem1N  39949  lhp2lt  39980  lhp2atne  40013  lhp2at0ne  40015  4atexlemunv  40045  4atexlemex2  40050  trlne  40164  trlval4  40167  cdlemc4  40173  cdleme11dN  40241  cdleme11h  40245  cdlemednuN  40279  cdleme20j  40297  cdleme20k  40298  cdleme21at  40307  cdleme35f  40433  cdlemg11b  40621  dia2dimlem1  41043  dihmeetlem3N  41284  dihmeetlem15N  41300  dochsnnz  41429  dochexmidlem1  41439  dochexmidlem7  41445  mapdindp3  41701  fltne  42617  pellexlem1  42802  dfac21  43039  pm13.14  44382  uzlidlring  48219  suppdm  48495