Theorem necon3ad 2795

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon1ad  2799  necon3d  2803  disjpss  3980  oeeulem  7568  enp1i  8080  canthp1lem2  9354  winalim2  9397  nlt1pi  9607  sqreulem  13947  rpnnen2lem11  14792  eucalglt  15136  nprm  15239  pcprmpw2  15424  pcmpt  15434  expnprm  15444  prmlem0  15650  pltnle  16789  psgnunilem1  17736  pgpfi  17843  frgpnabllem1  18099  gsumval3a  18127  ablfac1eulem  18294  pgpfaclem2  18304  lspdisjb  18947  lspdisj2  18948  obselocv  19891  0nnei  20726  t0dist  20939  t1sep  20984  ordthauslem  20997  hausflim  21595  bcthlem5  22933  bcth  22934  fta1g  23731  plyco0  23752  dgrnznn  23807  coeaddlem  23809  fta1  23867  vieta1lem2  23870  logcnlem3  24190  dvloglem  24194  dcubic  24373  mumullem2  24706  2sqlem8a  24950  dchrisum0flblem1  24997  colperpexlem2  25423  ocnel  27541  hatomistici  28605  sibfof  29729  outsideofrflx  31404  poimirlem23  32602  mblfinlem1  32616  cntotbnd  32765  heiborlem6  32785  lshpnel  33288  lshpcmp  33293  lfl1  33375  lkrshp  33410  lkrpssN  33468  atnlt  33618  atnle  33622  atlatmstc  33624  intnatN  33711  atbtwn  33750  llnnlt  33827  lplnnlt  33869  2llnjaN  33870  lvolnltN  33922  2lplnja  33923  dalem-cly  33975  dalem44  34020  2llnma3r  34092  cdlemblem  34097  lhpm0atN  34333  lhp2atnle  34337  cdlemednpq  34604  cdleme22cN  34648  cdlemg18b  34985  cdlemg42  35035  dia2dimlem1  35371  dochkrshp  35693  hgmapval0  36202  2f1fvneq  40322  1loopgrnb0  40717  usgr2trlncrct  41009