Theorem necon3ad 2951

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  necon1ad  2955  necon3d  2959  disjpss  4467  2f1fvneq  7280  oeeulem  8638  enp1iOLD  9312  canthp1lem2  10691  winalim2  10734  nlt1pi  10944  sqreulem  15395  rpnnen2lem11  16257  eucalglt  16619  nprm  16722  pcprmpw2  16916  pcmpt  16926  expnprm  16936  prmlem0  17140  pltnle  18396  psgnunilem1  19526  pgpfi  19638  frgpnabllem1  19906  gsumval3a  19936  ablfac1eulem  20107  pgpfaclem2  20117  ablsimpgfindlem1  20142  lspdisjb  21146  lspdisj2  21147  obselocv  21766  mhpmulcl  22171  0nnei  23136  t0dist  23349  t1sep  23394  ordthauslem  23407  hausflim  24005  bcthlem5  25376  bcth  25377  fta1g  26224  plyco0  26246  dgrnznn  26301  coeaddlem  26303  fta1  26365  vieta1lem2  26368  logcnlem3  26701  dvloglem  26705  dcubic  26904  mumullem2  27238  2sqlem8a  27484  dchrisum0flblem1  27567  colperpexlem2  28754  elntg2  29015  1loopgrnb0  29535  usgr2trlncrct  29836  ocnel  31327  hatomistici  32391  1arithufdlem4  33555  lbslsat  33644  sibfof  34322  outsideofrflx  36109  poimirlem23  37630  mblfinlem1  37644  cntotbnd  37783  heiborlem6  37803  lshpnel  38965  lshpcmp  38970  lfl1  39052  lkrshp  39087  lkrpssN  39145  atnlt  39295  atnle  39299  atlatmstc  39301  intnatN  39390  atbtwn  39429  llnnlt  39506  lplnnlt  39548  2llnjaN  39549  lvolnltN  39601  2lplnja  39602  dalem-cly  39654  dalem44  39699  2llnma3r  39771  cdlemblem  39776  lhpm0atN  40012  lhp2atnle  40016  cdlemednpq  40282  cdleme22cN  40325  cdlemg18b  40662  cdlemg42  40712  dia2dimlem1  41047  dochkrshp  41369  hgmapval0  41875  rrx2pnecoorneor  48565