Theorem necon3ad 2955

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  necon1ad  2959  necon3d  2963  disjpss  4391  2f1fvneq  7114  oeeulem  8394  enp1i  8982  canthp1lem2  10340  winalim2  10383  nlt1pi  10593  sqreulem  14999  rpnnen2lem11  15861  eucalglt  16218  nprm  16321  pcprmpw2  16511  pcmpt  16521  expnprm  16531  prmlem0  16735  pltnle  17971  psgnunilem1  19016  pgpfi  19125  frgpnabllem1  19389  gsumval3a  19419  ablfac1eulem  19590  pgpfaclem2  19600  ablsimpgfindlem1  19625  lspdisjb  20303  lspdisj2  20304  obselocv  20845  mhpmulcl  21249  0nnei  22171  t0dist  22384  t1sep  22429  ordthauslem  22442  hausflim  23040  bcthlem5  24397  bcth  24398  fta1g  25237  plyco0  25258  dgrnznn  25313  coeaddlem  25315  fta1  25373  vieta1lem2  25376  logcnlem3  25704  dvloglem  25708  dcubic  25901  mumullem2  26234  2sqlem8a  26478  dchrisum0flblem1  26561  colperpexlem2  26996  elntg2  27256  1loopgrnb0  27772  usgr2trlncrct  28072  ocnel  29561  hatomistici  30625  lbslsat  31601  sibfof  32207  outsideofrflx  34356  poimirlem23  35727  mblfinlem1  35741  cntotbnd  35881  heiborlem6  35901  lshpnel  36924  lshpcmp  36929  lfl1  37011  lkrshp  37046  lkrpssN  37104  atnlt  37254  atnle  37258  atlatmstc  37260  intnatN  37348  atbtwn  37387  llnnlt  37464  lplnnlt  37506  2llnjaN  37507  lvolnltN  37559  2lplnja  37560  dalem-cly  37612  dalem44  37657  2llnma3r  37729  cdlemblem  37734  lhpm0atN  37970  lhp2atnle  37974  cdlemednpq  38240  cdleme22cN  38283  cdlemg18b  38620  cdlemg42  38670  dia2dimlem1  39005  dochkrshp  39327  hgmapval0  39833  rrx2pnecoorneor  45949