Theorem necon3bd 2954

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 2944	. . 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 2940

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 2941

This theorem is referenced by:  necon2ad  2955  nssne1  4046  nssne2  4047  disjne  4455  nbrne1  5162  nbrne2  5163  peano5  7915  oeeui  8640  domdifsn  9094  ac6sfi  9320  inf3lem2  9669  cnfcom3lem  9743  dfac9  10177  fin23lem21  10379  dedekindle  11425  zneo  12701  modirr  13983  sqrmo  15290  reusq0  15501  pc2dvds  16917  pcadd  16927  oddprmdvds  16941  4sqlem11  16993  latnlej  18501  sylow2blem3  19640  irredn0  20423  irredn1  20426  isnzr2  20518  lssvneln0  20950  lspsnne2  21120  lspfixed  21130  lspindpi  21134  lsmcv  21143  lspsolv  21145  coe1tmmul  22280  dfac14  23626  fbdmn0  23842  filufint  23928  flimfnfcls  24036  alexsubALTlem2  24056  evth  24991  cphsqrtcl2  25220  ovolicc2lem4  25555  lhop1lem  26052  lhop1  26053  lhop2  26054  lhop  26055  deg1add  26142  abelthlem2  26476  logcnlem2  26685  angpined  26873  asinneg  26929  dmgmaddn0  27066  lgsne0  27379  lgsqr  27395  lgsquadlem2  27425  lgsquadlem3  27426  axlowdimlem17  28973  spansncvi  31671  zarcmplem  33880  broutsideof2  36123  unblimceq0lem  36507  poimirlem28  37655  dvasin  37711  dvacos  37712  nninfnub  37758  dvrunz  37961  lsatcvatlem  39050  lkrlsp2  39104  opnlen0  39189  2llnne2N  39410  lnnat  39429  llnn0  39518  lplnn0N  39549  lplnllnneN  39558  llncvrlpln2  39559  llncvrlpln  39560  lvoln0N  39593  lplncvrlvol2  39617  lplncvrlvol  39618  dalempnes  39653  dalemqnet  39654  dalemcea  39662  dalem3  39666  cdlema1N  39793  cdlemb  39796  paddasslem5  39826  llnexchb2lem  39870  osumcllem4N  39961  pexmidlem1N  39972  lhp2lt  40003  lhp2atne  40036  lhp2at0ne  40038  4atexlemunv  40068  4atexlemex2  40073  trlne  40187  trlval4  40190  cdlemc4  40196  cdleme11dN  40264  cdleme11h  40268  cdlemednuN  40302  cdleme20j  40320  cdleme20k  40321  cdleme21at  40330  cdleme35f  40456  cdlemg11b  40644  dia2dimlem1  41066  dihmeetlem3N  41307  dihmeetlem15N  41323  dochsnnz  41452  dochexmidlem1  41462  dochexmidlem7  41468  mapdindp3  41724  fltne  42654  pellexlem1  42840  dfac21  43078  pm13.14  44428  uzlidlring  48151  suppdm  48427