Theorem necon3ad 2964

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 2957	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
3	1, 2	nsyli 157	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1554   ≠ wne 2951

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 209  df-ne 2952

This theorem is referenced by:  necon1ad  2968  necon3d  2972  disjpss  4409  oeeulem  8559  canthp1lem2  10601  winalim2  10644  nlt1pi  10854  sqreulem  15363  rpnnen2lem11  16232  eucalglt  16595  nprm  16698  pcprmpw2  16894  pcmpt  16904  expnprm  16914  prmlem0  17117  pltnle  18344  psgnunilem1  19509  pgpfi  19621  frgpnabllem1  19889  gsumval3a  19919  ablfac1eulem  20090  pgpfaclem2  20100  ablsimpgfindlem1  20125  lspdisjb  21169  lspdisj2  21170  obselocv  21753  mhpmulcl  22187  0nnei  23145  t0dist  23358  t1sep  23403  ordthauslem  23416  hausflim  24014  bcthlem5  25363  bcth  25364  fta1g  26203  plyco0  26225  dgrnznn  26280  coeaddlem  26282  fta1  26342  vieta1lem2  26345  logcnlem3  26679  dvloglem  26683  dcubic  26881  mumullem2  27214  2sqlem8a  27459  dchrisum0flblem1  27542  colperpexlem2  28870  elntg2  29125  1loopgrnb0  29642  usgr2trlncrct  29945  ocnel  31440  hatomistici  32504  1arithufdlem4  33697  lbslsat  33867  sibfof  34591  outsideofrflx  36425  poimirlem23  38090  mblfinlem1  38104  cntotbnd  38243  heiborlem6  38263  lshpnel  39555  lshpcmp  39560  lfl1  39642  lkrshp  39677  lkrpssN  39735  atnlt  39885  atnle  39889  atlatmstc  39891  intnatN  39979  atbtwn  40018  llnnlt  40095  lplnnlt  40137  2llnjaN  40138  lvolnltN  40190  2lplnja  40191  dalem-cly  40243  dalem44  40288  2llnma3r  40360  cdlemblem  40365  lhpm0atN  40601  lhp2atnle  40605  cdlemednpq  40871  cdleme22cN  40914  cdlemg18b  41251  cdlemg42  41301  dia2dimlem1  41636  dochkrshp  41958  hgmapval0  42464  rrx2pnecoorneor  49285