Theorem necon3ad 3000

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  necon1ad  3004  necon3d  3008  disjpss  4368  2f1fvneq  6996  oeeulem  8210  enp1i  8737  canthp1lem2  10064  winalim2  10107  nlt1pi  10317  sqreulem  14711  rpnnen2lem11  15569  eucalglt  15919  nprm  16022  pcprmpw2  16208  pcmpt  16218  expnprm  16228  prmlem0  16431  pltnle  17568  psgnunilem1  18613  pgpfi  18722  frgpnabllem1  18986  gsumval3a  19016  ablfac1eulem  19187  pgpfaclem2  19197  ablsimpgfindlem1  19222  lspdisjb  19891  lspdisj2  19892  obselocv  20417  0nnei  21717  t0dist  21930  t1sep  21975  ordthauslem  21988  hausflim  22586  bcthlem5  23932  bcth  23933  fta1g  24768  plyco0  24789  dgrnznn  24844  coeaddlem  24846  fta1  24904  vieta1lem2  24907  logcnlem3  25235  dvloglem  25239  dcubic  25432  mumullem2  25765  2sqlem8a  26009  dchrisum0flblem1  26092  colperpexlem2  26525  elntg2  26779  1loopgrnb0  27292  usgr2trlncrct  27592  ocnel  29081  hatomistici  30145  lbslsat  31102  sibfof  31708  outsideofrflx  33701  poimirlem23  35080  mblfinlem1  35094  cntotbnd  35234  heiborlem6  35254  lshpnel  36279  lshpcmp  36284  lfl1  36366  lkrshp  36401  lkrpssN  36459  atnlt  36609  atnle  36613  atlatmstc  36615  intnatN  36703  atbtwn  36742  llnnlt  36819  lplnnlt  36861  2llnjaN  36862  lvolnltN  36914  2lplnja  36915  dalem-cly  36967  dalem44  37012  2llnma3r  37084  cdlemblem  37089  lhpm0atN  37325  lhp2atnle  37329  cdlemednpq  37595  cdleme22cN  37638  cdlemg18b  37975  cdlemg42  38025  dia2dimlem1  38360  dochkrshp  38682  hgmapval0  39188  rrx2pnecoorneor  45129