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 1540   ≠ 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  4441  oeeulem  8618  enp1iOLD  9291  canthp1lem2  10672  winalim2  10715  nlt1pi  10925  sqreulem  15383  rpnnen2lem11  16247  eucalglt  16609  nprm  16712  pcprmpw2  16907  pcmpt  16917  expnprm  16927  prmlem0  17130  pltnle  18353  psgnunilem1  19479  pgpfi  19591  frgpnabllem1  19859  gsumval3a  19889  ablfac1eulem  20060  pgpfaclem2  20070  ablsimpgfindlem1  20095  lspdisjb  21092  lspdisj2  21093  obselocv  21693  mhpmulcl  22092  0nnei  23055  t0dist  23268  t1sep  23313  ordthauslem  23326  hausflim  23924  bcthlem5  25285  bcth  25286  fta1g  26132  plyco0  26154  dgrnznn  26209  coeaddlem  26211  fta1  26273  vieta1lem2  26276  logcnlem3  26610  dvloglem  26614  dcubic  26813  mumullem2  27147  2sqlem8a  27393  dchrisum0flblem1  27476  colperpexlem2  28715  elntg2  28969  1loopgrnb0  29487  usgr2trlncrct  29793  ocnel  31284  hatomistici  32348  1arithufdlem4  33567  lbslsat  33661  sibfof  34377  outsideofrflx  36150  poimirlem23  37672  mblfinlem1  37686  cntotbnd  37825  heiborlem6  37845  lshpnel  39006  lshpcmp  39011  lfl1  39093  lkrshp  39128  lkrpssN  39186  atnlt  39336  atnle  39340  atlatmstc  39342  intnatN  39431  atbtwn  39470  llnnlt  39547  lplnnlt  39589  2llnjaN  39590  lvolnltN  39642  2lplnja  39643  dalem-cly  39695  dalem44  39740  2llnma3r  39812  cdlemblem  39817  lhpm0atN  40053  lhp2atnle  40057  cdlemednpq  40323  cdleme22cN  40366  cdlemg18b  40703  cdlemg42  40753  dia2dimlem1  41088  dochkrshp  41410  hgmapval0  41916  rrx2pnecoorneor  48662