Theorem necon3bd 2960

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon2ad  2961  nssne1  4071  nssne2  4072  disjne  4478  nbrne1  5185  nbrne2  5186  peano5  7932  peano5OLD  7933  oeeui  8658  domdifsn  9120  ac6sfi  9348  inf3lem2  9698  cnfcom3lem  9772  dfac9  10206  fin23lem21  10408  dedekindle  11454  zneo  12726  modirr  13993  sqrmo  15300  reusq0  15511  pc2dvds  16926  pcadd  16936  oddprmdvds  16950  4sqlem11  17002  latnlej  18526  sylow2blem3  19664  irredn0  20449  irredn1  20452  isnzr2  20544  lssvneln0  20973  lspsnne2  21143  lspfixed  21153  lspindpi  21157  lsmcv  21166  lspsolv  21168  coe1tmmul  22301  dfac14  23647  fbdmn0  23863  filufint  23949  flimfnfcls  24057  alexsubALTlem2  24077  evth  25010  cphsqrtcl2  25239  ovolicc2lem4  25574  lhop1lem  26072  lhop1  26073  lhop2  26074  lhop  26075  deg1add  26162  abelthlem2  26494  logcnlem2  26703  angpined  26891  asinneg  26947  dmgmaddn0  27084  lgsne0  27397  lgsqr  27413  lgsquadlem2  27443  lgsquadlem3  27444  axlowdimlem17  28991  spansncvi  31684  zarcmplem  33827  broutsideof2  36086  unblimceq0lem  36472  poimirlem28  37608  dvasin  37664  dvacos  37665  nninfnub  37711  dvrunz  37914  lsatcvatlem  39005  lkrlsp2  39059  opnlen0  39144  2llnne2N  39365  lnnat  39384  llnn0  39473  lplnn0N  39504  lplnllnneN  39513  llncvrlpln2  39514  llncvrlpln  39515  lvoln0N  39548  lplncvrlvol2  39572  lplncvrlvol  39573  dalempnes  39608  dalemqnet  39609  dalemcea  39617  dalem3  39621  cdlema1N  39748  cdlemb  39751  paddasslem5  39781  llnexchb2lem  39825  osumcllem4N  39916  pexmidlem1N  39927  lhp2lt  39958  lhp2atne  39991  lhp2at0ne  39993  4atexlemunv  40023  4atexlemex2  40028  trlne  40142  trlval4  40145  cdlemc4  40151  cdleme11dN  40219  cdleme11h  40223  cdlemednuN  40257  cdleme20j  40275  cdleme20k  40276  cdleme21at  40285  cdleme35f  40411  cdlemg11b  40599  dia2dimlem1  41021  dihmeetlem3N  41262  dihmeetlem15N  41278  dochsnnz  41407  dochexmidlem1  41417  dochexmidlem7  41423  mapdindp3  41679  fltne  42599  pellexlem1  42785  dfac21  43023  pm13.14  44378  uzlidlring  47958  suppdm  48239