Theorem necon3ad 2948

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ≠ wne 2935

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 206  df-ne 2936

This theorem is referenced by:  necon1ad  2952  necon3d  2956  disjpss  4456  2f1fvneq  7264  oeeulem  8615  enp1iOLD  9296  canthp1lem2  10668  winalim2  10711  nlt1pi  10921  sqreulem  15330  rpnnen2lem11  16192  eucalglt  16547  nprm  16650  pcprmpw2  16842  pcmpt  16852  expnprm  16862  prmlem0  17066  pltnle  18321  psgnunilem1  19439  pgpfi  19551  frgpnabllem1  19819  gsumval3a  19849  ablfac1eulem  20020  pgpfaclem2  20030  ablsimpgfindlem1  20055  lspdisjb  21003  lspdisj2  21004  obselocv  21649  mhpmulcl  22060  0nnei  23003  t0dist  23216  t1sep  23261  ordthauslem  23274  hausflim  23872  bcthlem5  25243  bcth  25244  fta1g  26091  plyco0  26113  dgrnznn  26168  coeaddlem  26170  fta1  26230  vieta1lem2  26233  logcnlem3  26565  dvloglem  26569  dcubic  26765  mumullem2  27099  2sqlem8a  27345  dchrisum0flblem1  27428  colperpexlem2  28522  elntg2  28783  1loopgrnb0  29303  usgr2trlncrct  29604  ocnel  31095  hatomistici  32159  lbslsat  33246  sibfof  33896  outsideofrflx  35659  poimirlem23  37051  mblfinlem1  37065  cntotbnd  37204  heiborlem6  37224  lshpnel  38392  lshpcmp  38397  lfl1  38479  lkrshp  38514  lkrpssN  38572  atnlt  38722  atnle  38726  atlatmstc  38728  intnatN  38817  atbtwn  38856  llnnlt  38933  lplnnlt  38975  2llnjaN  38976  lvolnltN  39028  2lplnja  39029  dalem-cly  39081  dalem44  39126  2llnma3r  39198  cdlemblem  39203  lhpm0atN  39439  lhp2atnle  39443  cdlemednpq  39709  cdleme22cN  39752  cdlemg18b  40089  cdlemg42  40139  dia2dimlem1  40474  dochkrshp  40796  hgmapval0  41302  rrx2pnecoorneor  47711