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  4415  oeeulem  8539  canthp1lem2  10576  winalim2  10619  nlt1pi  10829  sqreulem  15295  rpnnen2lem11  16161  eucalglt  16524  nprm  16627  pcprmpw2  16822  pcmpt  16832  expnprm  16842  prmlem0  17045  pltnle  18271  psgnunilem1  19434  pgpfi  19546  frgpnabllem1  19814  gsumval3a  19844  ablfac1eulem  20015  pgpfaclem2  20025  ablsimpgfindlem1  20050  lspdisjb  21093  lspdisj2  21094  obselocv  21695  mhpmulcl  22104  0nnei  23068  t0dist  23281  t1sep  23326  ordthauslem  23339  hausflim  23937  bcthlem5  25296  bcth  25297  fta1g  26143  plyco0  26165  dgrnznn  26220  coeaddlem  26222  fta1  26284  vieta1lem2  26287  logcnlem3  26621  dvloglem  26625  dcubic  26824  mumullem2  27158  2sqlem8a  27404  dchrisum0flblem1  27487  colperpexlem2  28815  elntg2  29070  1loopgrnb0  29588  usgr2trlncrct  29891  ocnel  31385  hatomistici  32449  1arithufdlem4  33639  lbslsat  33793  sibfof  34517  outsideofrflx  36340  poimirlem23  37883  mblfinlem1  37897  cntotbnd  38036  heiborlem6  38056  lshpnel  39348  lshpcmp  39353  lfl1  39435  lkrshp  39470  lkrpssN  39528  atnlt  39678  atnle  39682  atlatmstc  39684  intnatN  39772  atbtwn  39811  llnnlt  39888  lplnnlt  39930  2llnjaN  39931  lvolnltN  39983  2lplnja  39984  dalem-cly  40036  dalem44  40081  2llnma3r  40153  cdlemblem  40158  lhpm0atN  40394  lhp2atnle  40398  cdlemednpq  40664  cdleme22cN  40707  cdlemg18b  41044  cdlemg42  41094  dia2dimlem1  41429  dochkrshp  41751  hgmapval0  42257  rrx2pnecoorneor  49064