Theorem necon3bd 2947

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 2937	. . 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 2933

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 2934

This theorem is referenced by:  necon2ad  2948  nssne1  3985  nssne2  3986  disjne  4396  nbrne1  5105  nbrne2  5106  peano5  7837  oeeui  8531  domdifsn  8991  ac6sfi  9187  inf3lem2  9541  cnfcom3lem  9615  dfac9  10050  fin23lem21  10252  1re  11135  dedekindle  11301  zneo  12603  modirr  13895  sqrmo  15204  reusq0  15418  pc2dvds  16841  pcadd  16851  oddprmdvds  16865  4sqlem11  16917  latnlej  18413  sylow2blem3  19588  irredn0  20394  irredn1  20397  isnzr2  20486  lssvneln0  20938  lspsnne2  21108  lspfixed  21118  lspindpi  21122  lsmcv  21131  lspsolv  21133  coe1tmmul  22252  dfac14  23593  fbdmn0  23809  filufint  23895  flimfnfcls  24003  alexsubALTlem2  24023  evth  24936  cphsqrtcl2  25163  ovolicc2lem4  25497  lhop1lem  25990  lhop1  25991  lhop2  25992  lhop  25993  deg1add  26078  abelthlem2  26410  logcnlem2  26620  angpined  26807  asinneg  26863  dmgmaddn0  27000  lgsne0  27312  lgsqr  27328  lgsquadlem2  27358  lgsquadlem3  27359  axlowdimlem17  29041  spansncvi  31738  argcj  32836  constrrecl  33929  zarcmplem  34041  broutsideof2  36320  unblimceq0lem  36782  poimirlem28  37983  dvasin  38039  dvacos  38040  nninfnub  38086  dvrunz  38289  lsatcvatlem  39509  lkrlsp2  39563  opnlen0  39648  2llnne2N  39868  lnnat  39887  llnn0  39976  lplnn0N  40007  lplnllnneN  40016  llncvrlpln2  40017  llncvrlpln  40018  lvoln0N  40051  lplncvrlvol2  40075  lplncvrlvol  40076  dalempnes  40111  dalemqnet  40112  dalemcea  40120  dalem3  40124  cdlema1N  40251  cdlemb  40254  paddasslem5  40284  llnexchb2lem  40328  osumcllem4N  40419  pexmidlem1N  40430  lhp2lt  40461  lhp2atne  40494  lhp2at0ne  40496  4atexlemunv  40526  4atexlemex2  40531  trlne  40645  trlval4  40648  cdlemc4  40654  cdleme11dN  40722  cdleme11h  40726  cdlemednuN  40760  cdleme20j  40778  cdleme20k  40779  cdleme21at  40788  cdleme35f  40914  cdlemg11b  41102  dia2dimlem1  41524  dihmeetlem3N  41765  dihmeetlem15N  41781  dochsnnz  41910  dochexmidlem1  41920  dochexmidlem7  41926  mapdindp3  42182  fltne  43091  pellexlem1  43275  dfac21  43512  pm13.14  44854  uzlidlring  48723  suppdm  48998