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  8530  canthp1lem2  10567  winalim2  10610  nlt1pi  10820  sqreulem  15313  rpnnen2lem11  16182  eucalglt  16545  nprm  16648  pcprmpw2  16844  pcmpt  16854  expnprm  16864  prmlem0  17067  pltnle  18293  psgnunilem1  19459  pgpfi  19571  frgpnabllem1  19839  gsumval3a  19869  ablfac1eulem  20040  pgpfaclem2  20050  ablsimpgfindlem1  20075  lspdisjb  21116  lspdisj2  21117  obselocv  21718  mhpmulcl  22125  0nnei  23087  t0dist  23300  t1sep  23345  ordthauslem  23358  hausflim  23956  bcthlem5  25305  bcth  25306  fta1g  26145  plyco0  26167  dgrnznn  26222  coeaddlem  26224  fta1  26285  vieta1lem2  26288  logcnlem3  26621  dvloglem  26625  dcubic  26823  mumullem2  27157  2sqlem8a  27402  dchrisum0flblem1  27485  colperpexlem2  28813  elntg2  29068  1loopgrnb0  29586  usgr2trlncrct  29889  ocnel  31384  hatomistici  32448  1arithufdlem4  33622  lbslsat  33776  sibfof  34500  outsideofrflx  36325  poimirlem23  37978  mblfinlem1  37992  cntotbnd  38131  heiborlem6  38151  lshpnel  39443  lshpcmp  39448  lfl1  39530  lkrshp  39565  lkrpssN  39623  atnlt  39773  atnle  39777  atlatmstc  39779  intnatN  39867  atbtwn  39906  llnnlt  39983  lplnnlt  40025  2llnjaN  40026  lvolnltN  40078  2lplnja  40079  dalem-cly  40131  dalem44  40176  2llnma3r  40248  cdlemblem  40253  lhpm0atN  40489  lhp2atnle  40493  cdlemednpq  40759  cdleme22cN  40802  cdlemg18b  41139  cdlemg42  41189  dia2dimlem1  41524  dochkrshp  41846  hgmapval0  42352  rrx2pnecoorneor  49203