Theorem necon3bd 2956

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  necon2ad  2957  nssne1  3977  nssne2  3978  disjne  4385  nbrne1  5089  nbrne2  5090  peano5  7714  peano5OLD  7715  oeeui  8395  domdifsn  8795  ac6sfi  8988  inf3lem2  9317  cnfcom3lem  9391  dfac9  9823  fin23lem21  10026  dedekindle  11069  zneo  12333  modirr  13590  sqrmo  14891  reusq0  15102  pc2dvds  16508  pcadd  16518  oddprmdvds  16532  4sqlem11  16584  latnlej  18089  sylow2blem3  19142  irredn0  19860  irredn1  19863  lssvneln0  20128  lspsnne2  20295  lspfixed  20305  lspindpi  20309  lsmcv  20318  lspsolv  20320  isnzr2  20447  coe1tmmul  21358  dfac14  22677  fbdmn0  22893  filufint  22979  flimfnfcls  23087  alexsubALTlem2  23107  evth  24028  cphsqrtcl2  24255  ovolicc2lem4  24589  lhop1lem  25082  lhop1  25083  lhop2  25084  lhop  25085  deg1add  25173  abelthlem2  25496  logcnlem2  25703  angpined  25885  asinneg  25941  dmgmaddn0  26077  lgsne0  26388  lgsqr  26404  lgsquadlem2  26434  lgsquadlem3  26435  axlowdimlem17  27229  spansncvi  29915  zarcmplem  31733  broutsideof2  34351  unblimceq0lem  34613  poimirlem28  35732  dvasin  35788  dvacos  35789  nninfnub  35836  dvrunz  36039  lsatcvatlem  36990  lkrlsp2  37044  opnlen0  37129  2llnne2N  37349  lnnat  37368  llnn0  37457  lplnn0N  37488  lplnllnneN  37497  llncvrlpln2  37498  llncvrlpln  37499  lvoln0N  37532  lplncvrlvol2  37556  lplncvrlvol  37557  dalempnes  37592  dalemqnet  37593  dalemcea  37601  dalem3  37605  cdlema1N  37732  cdlemb  37735  paddasslem5  37765  llnexchb2lem  37809  osumcllem4N  37900  pexmidlem1N  37911  lhp2lt  37942  lhp2atne  37975  lhp2at0ne  37977  4atexlemunv  38007  4atexlemex2  38012  trlne  38126  trlval4  38129  cdlemc4  38135  cdleme11dN  38203  cdleme11h  38207  cdlemednuN  38241  cdleme20j  38259  cdleme20k  38260  cdleme21at  38269  cdleme35f  38395  cdlemg11b  38583  dia2dimlem1  39005  dihmeetlem3N  39246  dihmeetlem15N  39262  dochsnnz  39391  dochexmidlem1  39401  dochexmidlem7  39407  mapdindp3  39663  fltne  40397  pellexlem1  40567  dfac21  40807  pm13.14  41916  uzlidlring  45375  suppdm  45739