Theorem necon3bd 2969

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 2959	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
2		necon3bd.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3	1, 2	biimtrid 245	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
4	3	con1d 146	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  necon2ad  2970  nssne1  3970  nssne2  3971  disjne  4407  nbrne1  5123  nbrne2  5124  peano5  7905  oeeui  8614  domdifsn  9082  ac6sfi  9278  inf3lem2  9633  cnfcom3lem  9707  dfac9  10218  fin23lem21  10420  1re  11311  dedekindle  11477  zneo  12785  modirr  14088  sqrmo  15423  reusq0  15637  pc2dvds  17062  pcadd  17072  oddprmdvds  17086  4sqlem11  17138  latnlej  18635  sylow2blem3  19841  irredn0  20658  irredn1  20661  isnzr2  20773  lssvneln0  21232  lspsnne2  21401  lspfixed  21411  lspindpi  21415  lsmcv  21424  lspsolv  21426  coe1tmmul  22601  dfac14  23942  fbdmn0  24158  filufint  24244  flimfnfcls  24352  alexsubALTlem2  24372  evth  25285  cphsqrtcl2  25512  ovolicc2lem4  25846  lhop1lem  26338  lhop1  26339  lhop2  26340  lhop  26341  deg1add  26426  abelthlem2  26764  logcnlem2  26976  angpined  27163  asinneg  27219  dmgmaddn0  27355  lgsne0  27667  lgsqr  27683  lgsquadlem2  27713  lgsquadlem3  27714  fltne  27980  axlowdimlem17  29541  spansncvi  32259  tgextalem1inag  33075  argcj  33386  constrrecl  34447  zarcmplem  34559  nelscottrankgt  35803  broutsideof2  36979  unblimceq0lem  37464  poimirlem28  38659  dvasin  38715  dvacos  38716  nninfnub  38778  dvrunz  38981  lsatcvatlem  40199  lkrlsp2  40253  opnlen0  40338  2llnne2N  40558  lnnat  40577  llnn0  40666  lplnn0N  40697  lplnllnneN  40706  llncvrlpln2  40707  llncvrlpln  40708  lvoln0N  40741  lplncvrlvol2  40765  lplncvrlvol  40766  dalempnes  40801  dalemqnet  40802  dalemcea  40810  dalem3  40814  cdlema1N  40941  cdlemb  40944  paddasslem5  40974  llnexchb2lem  41018  osumcllem4N  41109  pexmidlem1N  41120  lhp2lt  41151  lhp2atne  41184  lhp2at0ne  41186  4atexlemunv  41216  4atexlemex2  41221  trlne  41335  trlval4  41338  cdlemc4  41344  cdleme11dN  41412  cdleme11h  41416  cdlemednuN  41450  cdleme20j  41468  cdleme20k  41469  cdleme21at  41478  cdleme35f  41604  cdlemg11b  41792  dia2dimlem1  42214  dihmeetlem3N  42455  dihmeetlem15N  42471  dochsnnz  42600  dochexmidlem1  42610  dochexmidlem7  42616  mapdindp3  42872  pellexlem1  43929  dfac21  44161  pm13.14  45486  uzlidlring  49425  suppdm  49715