Theorem necon3ad 2946

Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

Hypothesis

Ref	Expression
necon3ad.1	⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵))

Assertion

Ref	Expression
necon3ad	⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓))

Proof of Theorem necon3ad

Step	Hyp	Ref	Expression
1		necon3ad.1	. 2 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵))
2		neneq 2939	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
3	1, 2	nsyli 157	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon1ad  2950  necon3d  2954  disjpss  4414  oeeulem  8531  canthp1lem2  10568  winalim2  10611  nlt1pi  10821  sqreulem  15287  rpnnen2lem11  16153  eucalglt  16516  nprm  16619  pcprmpw2  16814  pcmpt  16824  expnprm  16834  prmlem0  17037  pltnle  18263  psgnunilem1  19426  pgpfi  19538  frgpnabllem1  19806  gsumval3a  19836  ablfac1eulem  20007  pgpfaclem2  20017  ablsimpgfindlem1  20042  lspdisjb  21085  lspdisj2  21086  obselocv  21687  mhpmulcl  22096  0nnei  23060  t0dist  23273  t1sep  23318  ordthauslem  23331  hausflim  23929  bcthlem5  25288  bcth  25289  fta1g  26135  plyco0  26157  dgrnznn  26212  coeaddlem  26214  fta1  26276  vieta1lem2  26279  logcnlem3  26613  dvloglem  26617  dcubic  26816  mumullem2  27150  2sqlem8a  27396  dchrisum0flblem1  27479  colperpexlem2  28786  elntg2  29041  1loopgrnb0  29559  usgr2trlncrct  29862  ocnel  31356  hatomistici  32420  1arithufdlem4  33609  lbslsat  33754  sibfof  34478  outsideofrflx  36302  poimirlem23  37815  mblfinlem1  37829  cntotbnd  37968  heiborlem6  37988  lshpnel  39280  lshpcmp  39285  lfl1  39367  lkrshp  39402  lkrpssN  39460  atnlt  39610  atnle  39614  atlatmstc  39616  intnatN  39704  atbtwn  39743  llnnlt  39820  lplnnlt  39862  2llnjaN  39863  lvolnltN  39915  2lplnja  39916  dalem-cly  39968  dalem44  40013  2llnma3r  40085  cdlemblem  40090  lhpm0atN  40326  lhp2atnle  40330  cdlemednpq  40596  cdleme22cN  40639  cdlemg18b  40976  cdlemg42  41026  dia2dimlem1  41361  dochkrshp  41683  hgmapval0  42189  rrx2pnecoorneor  48997