Theorem necon3bd 2970

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 2960	. . 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 1570   ≠ wne 2956

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 2957

This theorem is used by:  necon2ad  2971  nssne1  3993  nssne2  3994  disjne  4408  nbrne1  5124  nbrne2  5125  peano5  7894  oeeui  8595  domdifsn  9063  ac6sfi  9259  inf3lem2  9614  cnfcom3lem  9688  dfac9  10196  fin23lem21  10398  1re  11289  dedekindle  11455  zneo  12763  modirr  14065  sqrmo  15398  reusq0  15612  pc2dvds  17037  pcadd  17047  oddprmdvds  17061  4sqlem11  17113  latnlej  18610  sylow2blem3  19816  irredn0  20633  irredn1  20636  isnzr2  20748  lssvneln0  21207  lspsnne2  21376  lspfixed  21386  lspindpi  21390  lsmcv  21399  lspsolv  21401  coe1tmmul  22576  dfac14  23917  fbdmn0  24133  filufint  24219  flimfnfcls  24327  alexsubALTlem2  24347  evth  25260  cphsqrtcl2  25487  ovolicc2lem4  25821  lhop1lem  26313  lhop1  26314  lhop2  26315  lhop  26316  deg1add  26401  abelthlem2  26741  logcnlem2  26953  angpined  27140  asinneg  27196  dmgmaddn0  27332  lgsne0  27644  lgsqr  27660  lgsquadlem2  27690  lgsquadlem3  27691  fltne  27957  axlowdimlem17  29518  spansncvi  32236  argcj  33322  constrrecl  34383  zarcmplem  34495  nelscottrankgt  35727  broutsideof2  36857  unblimceq0lem  37342  poimirlem28  38534  dvasin  38590  dvacos  38591  nninfnub  38653  dvrunz  38856  lsatcvatlem  40074  lkrlsp2  40128  opnlen0  40213  2llnne2N  40433  lnnat  40452  llnn0  40541  lplnn0N  40572  lplnllnneN  40581  llncvrlpln2  40582  llncvrlpln  40583  lvoln0N  40616  lplncvrlvol2  40640  lplncvrlvol  40641  dalempnes  40676  dalemqnet  40677  dalemcea  40685  dalem3  40689  cdlema1N  40816  cdlemb  40819  paddasslem5  40849  llnexchb2lem  40893  osumcllem4N  40984  pexmidlem1N  40995  lhp2lt  41026  lhp2atne  41059  lhp2at0ne  41061  4atexlemunv  41091  4atexlemex2  41096  trlne  41210  trlval4  41213  cdlemc4  41219  cdleme11dN  41287  cdleme11h  41291  cdlemednuN  41325  cdleme20j  41343  cdleme20k  41344  cdleme21at  41353  cdleme35f  41479  cdlemg11b  41667  dia2dimlem1  42089  dihmeetlem3N  42330  dihmeetlem15N  42346  dochsnnz  42475  dochexmidlem1  42485  dochexmidlem7  42491  mapdindp3  42747  pellexlem1  43789  dfac21  44026  pm13.14  45352  uzlidlring  49276  suppdm  49566