Theorem necon3ad 2972

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2960

This theorem is used by:  necon1ad  2976  necon3d  2980  disjpss  4417  oeeulem  8638  canthp1lem2  10765  winalim2  10808  nlt1pi  11018  sqreulem  15556  rpnnen2lem11  16421  eucalglt  16789  nprm  16892  pcprmpw2  17089  pcmpt  17099  expnprm  17109  prmlem0  17312  pltnle  18539  psgnunilem1  19737  pgpfi  19849  frgpnabllem1  20117  gsumval3a  20147  ablfac1eulem  20318  pgpfaclem2  20328  ablsimpgfindlem1  20353  lspdisjb  21434  lspdisj2  21435  obselocv  22064  mhpmulcl  22500  0nnei  23460  t0dist  23673  t1sep  23718  ordthauslem  23731  hausflim  24330  bcthlem5  25679  bcth  25680  fta1g  26518  plyco0  26540  dgrnznn  26596  coeaddlem  26598  fta1  26659  vieta1lem2  26664  logcnlem3  27002  dvloglem  27006  dcubic  27204  mumullem2  27537  2sqlem8a  27782  dchrisum0flblem1  27865  colperpexlem2  29237  elntg2  29593  1loopgrnb0  30113  usgr2trlncrct  30425  ocnel  31930  hatomistici  32994  1arithufdlem4  34149  lbslsat  34318  sibfof  35042  outsideofrflx  37070  poimirlem23  38753  mblfinlem1  38767  cntotbnd  38922  heiborlem6  38942  lshpnel  40232  lshpcmp  40237  lfl1  40319  lkrshp  40354  lkrpssN  40412  atnlt  40562  atnle  40566  atlatmstc  40568  intnatN  40656  atbtwn  40695  llnnlt  40772  lplnnlt  40814  2llnjaN  40815  lvolnltN  40867  2lplnja  40868  dalem-cly  40920  dalem44  40965  2llnma3r  41037  cdlemblem  41042  lhpm0atN  41278  lhp2atnle  41282  cdlemednpq  41548  cdleme22cN  41591  cdlemg18b  41928  cdlemg42  41978  dia2dimlem1  42313  dochkrshp  42635  hgmapval0  43141  rrx2pnecoorneor  50033