Theorem necon3ad 2968

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2955

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 2956

This theorem is used by:  necon1ad  2972  necon3d  2976  disjpss  4413  oeeulem  8611  canthp1lem2  10739  winalim2  10782  nlt1pi  10992  sqreulem  15528  rpnnen2lem11  16393  eucalglt  16761  nprm  16864  pcprmpw2  17061  pcmpt  17071  expnprm  17081  prmlem0  17284  pltnle  18511  psgnunilem1  19708  pgpfi  19820  frgpnabllem1  20088  gsumval3a  20118  ablfac1eulem  20289  pgpfaclem2  20299  ablsimpgfindlem1  20324  lspdisjb  21405  lspdisj2  21406  obselocv  22035  mhpmulcl  22471  0nnei  23431  t0dist  23644  t1sep  23689  ordthauslem  23702  hausflim  24301  bcthlem5  25650  bcth  25651  fta1g  26489  plyco0  26511  dgrnznn  26567  coeaddlem  26569  fta1  26630  vieta1lem2  26635  logcnlem3  26973  dvloglem  26977  dcubic  27175  mumullem2  27508  2sqlem8a  27753  dchrisum0flblem1  27836  colperpexlem2  29208  elntg2  29564  1loopgrnb0  30084  usgr2trlncrct  30396  ocnel  31901  hatomistici  32965  1arithufdlem4  34122  lbslsat  34291  sibfof  35015  outsideofrflx  36967  poimirlem23  38637  mblfinlem1  38651  cntotbnd  38806  heiborlem6  38826  lshpnel  40116  lshpcmp  40121  lfl1  40203  lkrshp  40238  lkrpssN  40296  atnlt  40446  atnle  40450  atlatmstc  40452  intnatN  40540  atbtwn  40579  llnnlt  40656  lplnnlt  40698  2llnjaN  40699  lvolnltN  40751  2lplnja  40752  dalem-cly  40804  dalem44  40849  2llnma3r  40921  cdlemblem  40926  lhpm0atN  41162  lhp2atnle  41166  cdlemednpq  41432  cdleme22cN  41475  cdlemg18b  41812  cdlemg42  41862  dia2dimlem1  42197  dochkrshp  42519  hgmapval0  43025  rrx2pnecoorneor  49903