Theorem necon3ad 2973

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 2961

This theorem is referenced by:  necon1ad  2977  necon3d  2981  disjpss  4418  oeeulem  8575  canthp1lem2  10626  winalim2  10669  nlt1pi  10879  sqreulem  15401  rpnnen2lem11  16270  eucalglt  16633  nprm  16736  pcprmpw2  16932  pcmpt  16942  expnprm  16952  prmlem0  17155  pltnle  18382  psgnunilem1  19554  pgpfi  19666  frgpnabllem1  19934  gsumval3a  19964  ablfac1eulem  20135  pgpfaclem2  20145  ablsimpgfindlem1  20170  lspdisjb  21219  lspdisj2  21220  obselocv  21838  mhpmulcl  22272  0nnei  23230  t0dist  23443  t1sep  23488  ordthauslem  23501  hausflim  24099  bcthlem5  25448  bcth  25449  fta1g  26288  plyco0  26310  dgrnznn  26365  coeaddlem  26367  fta1  26430  vieta1lem2  26433  logcnlem3  26767  dvloglem  26771  dcubic  26969  mumullem2  27302  2sqlem8a  27547  dchrisum0flblem1  27630  colperpexlem2  28962  elntg2  29244  1loopgrnb0  29761  usgr2trlncrct  30064  ocnel  31559  hatomistici  32623  1arithufdlem4  33754  lbslsat  33923  sibfof  34647  outsideofrflx  36490  poimirlem23  38154  mblfinlem1  38168  cntotbnd  38307  heiborlem6  38327  lshpnel  39619  lshpcmp  39624  lfl1  39706  lkrshp  39741  lkrpssN  39799  atnlt  39949  atnle  39953  atlatmstc  39955  intnatN  40043  atbtwn  40082  llnnlt  40159  lplnnlt  40201  2llnjaN  40202  lvolnltN  40254  2lplnja  40255  dalem-cly  40307  dalem44  40352  2llnma3r  40424  cdlemblem  40429  lhpm0atN  40665  lhp2atnle  40669  cdlemednpq  40935  cdleme22cN  40978  cdlemg18b  41315  cdlemg42  41365  dia2dimlem1  41700  dochkrshp  42022  hgmapval0  42528  rrx2pnecoorneor  49346