Theorem necon3bd 2957

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 2947	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
2		necon3bd.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3	1, 2	syl5bi 232	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
4	3	con1d 141	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1631   ≠ wne 2943

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 197  df-ne 2944

This theorem is referenced by:  necon2ad  2958  nelne1  3039  nelne2  3040  nssne1  3810  nssne2  3811  disjne  4165  nbrne1  4805  nbrne2  4806  peano5  7236  oeeui  7836  domdifsn  8199  ac6sfi  8360  inf3lem2  8690  cnfcom3lem  8764  dfac9  9160  fin23lem21  9363  dedekindle  10403  zneo  11662  modirr  12949  sqrmo  14200  pc2dvds  15790  pcadd  15800  oddprmdvds  15814  4sqlem11  15866  latnlej  17276  sylow2blem3  18244  irredn0  18911  irredn1  18914  lssvneln0  19162  lssneln0OLD  19164  lspsnne2  19331  lspfixed  19341  lspfixedOLD  19342  lspindpi  19346  lsmcv  19355  lspsolv  19357  isnzr2  19478  coe1tmmul  19862  dfac14  21642  fbdmn0  21858  filufint  21944  flimfnfcls  22052  alexsubALTlem2  22072  evth  22978  cphsqrtcl2  23205  ovolicc2lem4  23508  lhop1lem  23996  lhop1  23997  lhop2  23998  lhop  23999  deg1add  24083  abelthlem2  24406  logcnlem2  24610  angpined  24778  asinneg  24834  dmgmaddn0  24970  lgsne0  25281  lgsqr  25297  lgsquadlem2  25327  lgsquadlem3  25328  axlowdimlem17  26059  spansncvi  28851  broutsideof2  32566  unblimceq0lem  32834  poimirlem28  33770  dvasin  33828  dvacos  33829  nninfnub  33879  dvrunz  34085  lsatcvatlem  34858  lkrlsp2  34912  opnlen0  34997  2llnne2N  35216  lnnat  35235  llnn0  35324  lplnn0N  35355  lplnllnneN  35364  llncvrlpln2  35365  llncvrlpln  35366  lvoln0N  35399  lplncvrlvol2  35423  lplncvrlvol  35424  dalempnes  35459  dalemqnet  35460  dalemcea  35468  dalem3  35472  cdlema1N  35599  cdlemb  35602  paddasslem5  35632  llnexchb2lem  35676  osumcllem4N  35767  pexmidlem1N  35778  lhp2lt  35809  lhp2atne  35842  lhp2at0ne  35844  4atexlemunv  35874  4atexlemex2  35879  trlne  35994  trlval4  35997  cdlemc4  36003  cdleme11dN  36071  cdleme11h  36075  cdlemednuN  36109  cdleme20j  36127  cdleme20k  36128  cdleme21at  36137  cdleme35f  36263  cdlemg11b  36451  dia2dimlem1  36874  dihmeetlem3N  37115  dihmeetlem15N  37131  dochsnnz  37260  dochexmidlem1  37270  dochexmidlem7  37276  mapdindp3  37532  pellexlem1  37919  dfac21  38162  pm13.14  39136  uzlidlring  42457  suppdm  42828