Theorem necon3ad 2946

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  necon1ad  2950  necon3d  2954  disjpss  4402  oeeulem  8537  canthp1lem2  10576  winalim2  10619  nlt1pi  10829  sqreulem  15322  rpnnen2lem11  16191  eucalglt  16554  nprm  16657  pcprmpw2  16853  pcmpt  16863  expnprm  16873  prmlem0  17076  pltnle  18302  psgnunilem1  19468  pgpfi  19580  frgpnabllem1  19848  gsumval3a  19878  ablfac1eulem  20049  pgpfaclem2  20059  ablsimpgfindlem1  20084  lspdisjb  21124  lspdisj2  21125  obselocv  21708  mhpmulcl  22115  0nnei  23077  t0dist  23290  t1sep  23335  ordthauslem  23348  hausflim  23946  bcthlem5  25295  bcth  25296  fta1g  26135  plyco0  26157  dgrnznn  26212  coeaddlem  26214  fta1  26274  vieta1lem2  26277  logcnlem3  26608  dvloglem  26612  dcubic  26810  mumullem2  27143  2sqlem8a  27388  dchrisum0flblem1  27471  colperpexlem2  28799  elntg2  29054  1loopgrnb0  29571  usgr2trlncrct  29874  ocnel  31369  hatomistici  32433  1arithufdlem4  33607  lbslsat  33760  sibfof  34484  outsideofrflx  36309  poimirlem23  37964  mblfinlem1  37978  cntotbnd  38117  heiborlem6  38137  lshpnel  39429  lshpcmp  39434  lfl1  39516  lkrshp  39551  lkrpssN  39609  atnlt  39759  atnle  39763  atlatmstc  39765  intnatN  39853  atbtwn  39892  llnnlt  39969  lplnnlt  40011  2llnjaN  40012  lvolnltN  40064  2lplnja  40065  dalem-cly  40117  dalem44  40162  2llnma3r  40234  cdlemblem  40239  lhpm0atN  40475  lhp2atnle  40479  cdlemednpq  40745  cdleme22cN  40788  cdlemg18b  41125  cdlemg42  41175  dia2dimlem1  41510  dochkrshp  41832  hgmapval0  42338  rrx2pnecoorneor  49185