Theorem necon3ad 2970

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 2963	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
3	1, 2	nsyli 158	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:  necon1ad  2974  necon3d  2978  disjpss  4417  oeeulem  8592  canthp1lem2  10665  winalim2  10708  nlt1pi  10918  sqreulem  15449  rpnnen2lem11  16316  eucalglt  16679  nprm  16782  pcprmpw2  16978  pcmpt  16988  expnprm  16998  prmlem0  17201  pltnle  18428  psgnunilem1  19624  pgpfi  19736  frgpnabllem1  20004  gsumval3a  20034  ablfac1eulem  20205  pgpfaclem2  20215  ablsimpgfindlem1  20240  lspdisjb  21317  lspdisj2  21318  obselocv  21945  mhpmulcl  22381  0nnei  23341  t0dist  23554  t1sep  23599  ordthauslem  23612  hausflim  24211  bcthlem5  25560  bcth  25561  fta1g  26400  plyco0  26422  dgrnznn  26477  coeaddlem  26479  fta1  26542  vieta1lem2  26545  logcnlem3  26882  dvloglem  26886  dcubic  27084  mumullem2  27417  2sqlem8a  27662  dchrisum0flblem1  27745  colperpexlem2  29087  elntg2  29443  1loopgrnb0  29963  usgr2trlncrct  30275  ocnel  31780  hatomistici  32844  1arithufdlem4  33959  lbslsat  34128  sibfof  34853  outsideofrflx  36709  poimirlem23  38394  mblfinlem1  38408  cntotbnd  38548  heiborlem6  38568  lshpnel  39858  lshpcmp  39863  lfl1  39945  lkrshp  39980  lkrpssN  40038  atnlt  40188  atnle  40192  atlatmstc  40194  intnatN  40282  atbtwn  40321  llnnlt  40398  lplnnlt  40440  2llnjaN  40441  lvolnltN  40493  2lplnja  40494  dalem-cly  40546  dalem44  40591  2llnma3r  40663  cdlemblem  40668  lhpm0atN  40904  lhp2atnle  40908  cdlemednpq  41174  cdleme22cN  41217  cdlemg18b  41554  cdlemg42  41604  dia2dimlem1  41939  dochkrshp  42261  hgmapval0  42767  rrx2pnecoorneor  49647