Theorem necon3bd 2946

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 2936	. . 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 2932

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 2933

This theorem is referenced by:  necon2ad  2947  nssne1  3996  nssne2  3997  disjne  4407  nbrne1  5117  nbrne2  5118  peano5  7835  oeeui  8530  domdifsn  8988  ac6sfi  9184  inf3lem2  9538  cnfcom3lem  9612  dfac9  10047  fin23lem21  10249  1re  11132  dedekindle  11297  zneo  12575  modirr  13865  sqrmo  15174  reusq0  15388  pc2dvds  16807  pcadd  16817  oddprmdvds  16831  4sqlem11  16883  latnlej  18379  sylow2blem3  19551  irredn0  20359  irredn1  20362  isnzr2  20451  lssvneln0  20903  lspsnne2  21073  lspfixed  21083  lspindpi  21087  lsmcv  21096  lspsolv  21098  coe1tmmul  22219  dfac14  23562  fbdmn0  23778  filufint  23864  flimfnfcls  23972  alexsubALTlem2  23992  evth  24914  cphsqrtcl2  25142  ovolicc2lem4  25477  lhop1lem  25974  lhop1  25975  lhop2  25976  lhop  25977  deg1add  26064  abelthlem2  26398  logcnlem2  26608  angpined  26796  asinneg  26852  dmgmaddn0  26989  lgsne0  27302  lgsqr  27318  lgsquadlem2  27348  lgsquadlem3  27349  axlowdimlem17  29031  spansncvi  31727  argcj  32828  constrrecl  33926  zarcmplem  34038  broutsideof2  36316  unblimceq0lem  36706  poimirlem28  37849  dvasin  37905  dvacos  37906  nninfnub  37952  dvrunz  38155  lsatcvatlem  39309  lkrlsp2  39363  opnlen0  39448  2llnne2N  39668  lnnat  39687  llnn0  39776  lplnn0N  39807  lplnllnneN  39816  llncvrlpln2  39817  llncvrlpln  39818  lvoln0N  39851  lplncvrlvol2  39875  lplncvrlvol  39876  dalempnes  39911  dalemqnet  39912  dalemcea  39920  dalem3  39924  cdlema1N  40051  cdlemb  40054  paddasslem5  40084  llnexchb2lem  40128  osumcllem4N  40219  pexmidlem1N  40230  lhp2lt  40261  lhp2atne  40294  lhp2at0ne  40296  4atexlemunv  40326  4atexlemex2  40331  trlne  40445  trlval4  40448  cdlemc4  40454  cdleme11dN  40522  cdleme11h  40526  cdlemednuN  40560  cdleme20j  40578  cdleme20k  40579  cdleme21at  40588  cdleme35f  40714  cdlemg11b  40902  dia2dimlem1  41324  dihmeetlem3N  41565  dihmeetlem15N  41581  dochsnnz  41710  dochexmidlem1  41720  dochexmidlem7  41726  mapdindp3  41982  fltne  42887  pellexlem1  43071  dfac21  43308  pm13.14  44650  uzlidlring  48481  suppdm  48756