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  4402  oeeulem  8528  canthp1lem2  10565  winalim2  10608  nlt1pi  10818  sqreulem  15311  rpnnen2lem11  16180  eucalglt  16543  nprm  16646  pcprmpw2  16842  pcmpt  16852  expnprm  16862  prmlem0  17065  pltnle  18291  psgnunilem1  19457  pgpfi  19569  frgpnabllem1  19837  gsumval3a  19867  ablfac1eulem  20038  pgpfaclem2  20048  ablsimpgfindlem1  20073  lspdisjb  21114  lspdisj2  21115  obselocv  21716  mhpmulcl  22124  0nnei  23086  t0dist  23299  t1sep  23344  ordthauslem  23357  hausflim  23955  bcthlem5  25304  bcth  25305  fta1g  26147  plyco0  26169  dgrnznn  26224  coeaddlem  26226  fta1  26287  vieta1lem2  26290  logcnlem3  26624  dvloglem  26628  dcubic  26827  mumullem2  27161  2sqlem8a  27407  dchrisum0flblem1  27490  colperpexlem2  28818  elntg2  29073  1loopgrnb0  29591  usgr2trlncrct  29894  ocnel  31389  hatomistici  32453  1arithufdlem4  33627  lbslsat  33781  sibfof  34505  outsideofrflx  36330  poimirlem23  37975  mblfinlem1  37989  cntotbnd  38128  heiborlem6  38148  lshpnel  39440  lshpcmp  39445  lfl1  39527  lkrshp  39562  lkrpssN  39620  atnlt  39770  atnle  39774  atlatmstc  39776  intnatN  39864  atbtwn  39903  llnnlt  39980  lplnnlt  40022  2llnjaN  40023  lvolnltN  40075  2lplnja  40076  dalem-cly  40128  dalem44  40173  2llnma3r  40245  cdlemblem  40250  lhpm0atN  40486  lhp2atnle  40490  cdlemednpq  40756  cdleme22cN  40799  cdlemg18b  41136  cdlemg42  41186  dia2dimlem1  41521  dochkrshp  41843  hgmapval0  42349  rrx2pnecoorneor  49188