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 1540   ≠ 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  4021  nssne2  4022  disjne  4430  nbrne1  5138  nbrne2  5139  peano5  7889  oeeui  8614  domdifsn  9068  ac6sfi  9292  inf3lem2  9643  cnfcom3lem  9717  dfac9  10151  fin23lem21  10353  dedekindle  11399  zneo  12676  modirr  13960  sqrmo  15270  reusq0  15481  pc2dvds  16899  pcadd  16909  oddprmdvds  16923  4sqlem11  16975  latnlej  18466  sylow2blem3  19603  irredn0  20383  irredn1  20386  isnzr2  20478  lssvneln0  20909  lspsnne2  21079  lspfixed  21089  lspindpi  21093  lsmcv  21102  lspsolv  21104  coe1tmmul  22214  dfac14  23556  fbdmn0  23772  filufint  23858  flimfnfcls  23966  alexsubALTlem2  23986  evth  24909  cphsqrtcl2  25138  ovolicc2lem4  25473  lhop1lem  25970  lhop1  25971  lhop2  25972  lhop  25973  deg1add  26060  abelthlem2  26394  logcnlem2  26604  angpined  26792  asinneg  26848  dmgmaddn0  26985  lgsne0  27298  lgsqr  27314  lgsquadlem2  27344  lgsquadlem3  27345  axlowdimlem17  28937  spansncvi  31633  argcj  32726  constrrecl  33803  zarcmplem  33912  broutsideof2  36140  unblimceq0lem  36524  poimirlem28  37672  dvasin  37728  dvacos  37729  nninfnub  37775  dvrunz  37978  lsatcvatlem  39067  lkrlsp2  39121  opnlen0  39206  2llnne2N  39427  lnnat  39446  llnn0  39535  lplnn0N  39566  lplnllnneN  39575  llncvrlpln2  39576  llncvrlpln  39577  lvoln0N  39610  lplncvrlvol2  39634  lplncvrlvol  39635  dalempnes  39670  dalemqnet  39671  dalemcea  39679  dalem3  39683  cdlema1N  39810  cdlemb  39813  paddasslem5  39843  llnexchb2lem  39887  osumcllem4N  39978  pexmidlem1N  39989  lhp2lt  40020  lhp2atne  40053  lhp2at0ne  40055  4atexlemunv  40085  4atexlemex2  40090  trlne  40204  trlval4  40207  cdlemc4  40213  cdleme11dN  40281  cdleme11h  40285  cdlemednuN  40319  cdleme20j  40337  cdleme20k  40338  cdleme21at  40347  cdleme35f  40473  cdlemg11b  40661  dia2dimlem1  41083  dihmeetlem3N  41324  dihmeetlem15N  41340  dochsnnz  41469  dochexmidlem1  41479  dochexmidlem7  41485  mapdindp3  41741  fltne  42667  pellexlem1  42852  dfac21  43090  pm13.14  44433  uzlidlring  48210  suppdm  48486