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 241	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
4	3	con1d 145	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ 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 206  df-ne 2941

This theorem is referenced by:  necon2ad  2955  nssne1  4044  nssne2  4045  disjne  4454  nbrne1  5167  nbrne2  5168  peano5  7886  peano5OLD  7887  oeeui  8604  domdifsn  9056  ac6sfi  9289  inf3lem2  9626  cnfcom3lem  9700  dfac9  10133  fin23lem21  10336  dedekindle  11382  zneo  12649  modirr  13911  sqrmo  15202  reusq0  15413  pc2dvds  16816  pcadd  16826  oddprmdvds  16840  4sqlem11  16892  latnlej  18413  sylow2blem3  19531  irredn0  20314  irredn1  20317  isnzr2  20409  lssvneln0  20706  lspsnne2  20876  lspfixed  20886  lspindpi  20890  lsmcv  20899  lspsolv  20901  coe1tmmul  22019  dfac14  23342  fbdmn0  23558  filufint  23644  flimfnfcls  23752  alexsubALTlem2  23772  evth  24699  cphsqrtcl2  24927  ovolicc2lem4  25261  lhop1lem  25754  lhop1  25755  lhop2  25756  lhop  25757  deg1add  25845  abelthlem2  26168  logcnlem2  26375  angpined  26559  asinneg  26615  dmgmaddn0  26751  lgsne0  27062  lgsqr  27078  lgsquadlem2  27108  lgsquadlem3  27109  axlowdimlem17  28471  spansncvi  31160  zarcmplem  33147  broutsideof2  35386  unblimceq0lem  35685  poimirlem28  36819  dvasin  36875  dvacos  36876  nninfnub  36922  dvrunz  37125  lsatcvatlem  38222  lkrlsp2  38276  opnlen0  38361  2llnne2N  38582  lnnat  38601  llnn0  38690  lplnn0N  38721  lplnllnneN  38730  llncvrlpln2  38731  llncvrlpln  38732  lvoln0N  38765  lplncvrlvol2  38789  lplncvrlvol  38790  dalempnes  38825  dalemqnet  38826  dalemcea  38834  dalem3  38838  cdlema1N  38965  cdlemb  38968  paddasslem5  38998  llnexchb2lem  39042  osumcllem4N  39133  pexmidlem1N  39144  lhp2lt  39175  lhp2atne  39208  lhp2at0ne  39210  4atexlemunv  39240  4atexlemex2  39245  trlne  39359  trlval4  39362  cdlemc4  39368  cdleme11dN  39436  cdleme11h  39440  cdlemednuN  39474  cdleme20j  39492  cdleme20k  39493  cdleme21at  39502  cdleme35f  39628  cdlemg11b  39816  dia2dimlem1  40238  dihmeetlem3N  40479  dihmeetlem15N  40495  dochsnnz  40624  dochexmidlem1  40634  dochexmidlem7  40640  mapdindp3  40896  fltne  41688  pellexlem1  41869  dfac21  42110  pm13.14  43470  uzlidlring  46916  suppdm  47279