Theorem necon3bd 2971

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 2961	. . 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 2957

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 2958

This theorem is used by:  necon2ad  2972  nssne1  3996  nssne2  3997  disjne  4411  nbrne1  5128  nbrne2  5129  peano5  7894  oeeui  8594  domdifsn  9062  ac6sfi  9258  inf3lem2  9612  cnfcom3lem  9686  dfac9  10143  fin23lem21  10345  1re  11236  dedekindle  11402  zneo  12708  modirr  14010  sqrmo  15342  reusq0  15556  pc2dvds  16977  pcadd  16987  oddprmdvds  17001  4sqlem11  17053  latnlej  18550  sylow2blem3  19755  irredn0  20570  irredn1  20573  isnzr2  20684  lssvneln0  21142  lspsnne2  21311  lspfixed  21321  lspindpi  21325  lsmcv  21334  lspsolv  21336  coe1tmmul  22509  dfac14  23850  fbdmn0  24066  filufint  24152  flimfnfcls  24260  alexsubALTlem2  24280  evth  25193  cphsqrtcl2  25420  ovolicc2lem4  25754  lhop1lem  26247  lhop1  26248  lhop2  26249  lhop  26250  deg1add  26335  abelthlem2  26675  logcnlem2  26888  angpined  27075  asinneg  27131  dmgmaddn0  27267  lgsne0  27579  lgsqr  27595  lgsquadlem2  27625  lgsquadlem3  27626  axlowdimlem17  29423  spansncvi  32141  argcj  33227  constrrecl  34287  zarcmplem  34399  nelscottrankgt  35640  broutsideof2  36710  unblimceq0lem  37211  poimirlem28  38405  dvasin  38461  dvacos  38462  nninfnub  38509  dvrunz  38712  lsatcvatlem  39930  lkrlsp2  39984  opnlen0  40069  2llnne2N  40289  lnnat  40308  llnn0  40397  lplnn0N  40428  lplnllnneN  40437  llncvrlpln2  40438  llncvrlpln  40439  lvoln0N  40472  lplncvrlvol2  40496  lplncvrlvol  40497  dalempnes  40532  dalemqnet  40533  dalemcea  40541  dalem3  40545  cdlema1N  40672  cdlemb  40675  paddasslem5  40705  llnexchb2lem  40749  osumcllem4N  40840  pexmidlem1N  40851  lhp2lt  40882  lhp2atne  40915  lhp2at0ne  40917  4atexlemunv  40947  4atexlemex2  40952  trlne  41066  trlval4  41069  cdlemc4  41075  cdleme11dN  41143  cdleme11h  41147  cdlemednuN  41181  cdleme20j  41199  cdleme20k  41200  cdleme21at  41209  cdleme35f  41335  cdlemg11b  41523  dia2dimlem1  41945  dihmeetlem3N  42186  dihmeetlem15N  42202  dochsnnz  42331  dochexmidlem1  42341  dochexmidlem7  42347  mapdindp3  42603  fltne  43498  pellexlem1  43678  dfac21  43915  pm13.14  45241  uzlidlring  49158  suppdm  49448