Theorem necon3bd 2942

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  necon2ad  2943  nssne1  3997  nssne2  3998  disjne  4405  nbrne1  5110  nbrne2  5111  peano5  7823  oeeui  8517  domdifsn  8973  ac6sfi  9168  inf3lem2  9519  cnfcom3lem  9593  dfac9  10028  fin23lem21  10230  1re  11112  dedekindle  11277  zneo  12556  modirr  13849  sqrmo  15158  reusq0  15372  pc2dvds  16791  pcadd  16801  oddprmdvds  16815  4sqlem11  16867  latnlej  18362  sylow2blem3  19535  irredn0  20342  irredn1  20345  isnzr2  20434  lssvneln0  20886  lspsnne2  21056  lspfixed  21066  lspindpi  21070  lsmcv  21079  lspsolv  21081  coe1tmmul  22192  dfac14  23534  fbdmn0  23750  filufint  23836  flimfnfcls  23944  alexsubALTlem2  23964  evth  24886  cphsqrtcl2  25114  ovolicc2lem4  25449  lhop1lem  25946  lhop1  25947  lhop2  25948  lhop  25949  deg1add  26036  abelthlem2  26370  logcnlem2  26580  angpined  26768  asinneg  26824  dmgmaddn0  26961  lgsne0  27274  lgsqr  27290  lgsquadlem2  27320  lgsquadlem3  27321  axlowdimlem17  28937  spansncvi  31630  argcj  32730  constrrecl  33780  zarcmplem  33892  broutsideof2  36162  unblimceq0lem  36546  poimirlem28  37694  dvasin  37750  dvacos  37751  nninfnub  37797  dvrunz  38000  lsatcvatlem  39094  lkrlsp2  39148  opnlen0  39233  2llnne2N  39453  lnnat  39472  llnn0  39561  lplnn0N  39592  lplnllnneN  39601  llncvrlpln2  39602  llncvrlpln  39603  lvoln0N  39636  lplncvrlvol2  39660  lplncvrlvol  39661  dalempnes  39696  dalemqnet  39697  dalemcea  39705  dalem3  39709  cdlema1N  39836  cdlemb  39839  paddasslem5  39869  llnexchb2lem  39913  osumcllem4N  40004  pexmidlem1N  40015  lhp2lt  40046  lhp2atne  40079  lhp2at0ne  40081  4atexlemunv  40111  4atexlemex2  40116  trlne  40230  trlval4  40233  cdlemc4  40239  cdleme11dN  40307  cdleme11h  40311  cdlemednuN  40345  cdleme20j  40363  cdleme20k  40364  cdleme21at  40373  cdleme35f  40499  cdlemg11b  40687  dia2dimlem1  41109  dihmeetlem3N  41350  dihmeetlem15N  41366  dochsnnz  41495  dochexmidlem1  41505  dochexmidlem7  41511  mapdindp3  41767  fltne  42683  pellexlem1  42868  dfac21  43105  pm13.14  44448  uzlidlring  48272  suppdm  48548