Theorem necon3ad 2969

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1568   ≠ wne 2956

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 210  df-ne 2957

This theorem is referenced by:  necon1ad  2973  necon3d  2977  disjpss  4420  oeeulem  8586  canthp1lem2  10637  winalim2  10680  nlt1pi  10890  sqreulem  15411  rpnnen2lem11  16279  eucalglt  16642  nprm  16745  pcprmpw2  16941  pcmpt  16951  expnprm  16961  prmlem0  17164  pltnle  18391  psgnunilem1  19562  pgpfi  19674  frgpnabllem1  19942  gsumval3a  19972  ablfac1eulem  20143  pgpfaclem2  20153  ablsimpgfindlem1  20178  lspdisjb  21229  lspdisj2  21230  obselocv  21857  mhpmulcl  22291  0nnei  23248  t0dist  23461  t1sep  23506  ordthauslem  23519  hausflim  24117  bcthlem5  25466  bcth  25467  fta1g  26306  plyco0  26328  dgrnznn  26383  coeaddlem  26385  fta1  26448  vieta1lem2  26451  logcnlem3  26785  dvloglem  26789  dcubic  26987  mumullem2  27320  2sqlem8a  27565  dchrisum0flblem1  27648  colperpexlem2  28987  elntg2  29301  1loopgrnb0  29818  usgr2trlncrct  30121  ocnel  31616  hatomistici  32680  1arithufdlem4  33803  lbslsat  33972  sibfof  34696  outsideofrflx  36585  poimirlem23  38260  mblfinlem1  38274  cntotbnd  38413  heiborlem6  38433  lshpnel  39725  lshpcmp  39730  lfl1  39812  lkrshp  39847  lkrpssN  39905  atnlt  40055  atnle  40059  atlatmstc  40061  intnatN  40149  atbtwn  40188  llnnlt  40265  lplnnlt  40307  2llnjaN  40308  lvolnltN  40360  2lplnja  40361  dalem-cly  40413  dalem44  40458  2llnma3r  40530  cdlemblem  40535  lhpm0atN  40771  lhp2atnle  40775  cdlemednpq  41041  cdleme22cN  41084  cdlemg18b  41421  cdlemg42  41471  dia2dimlem1  41806  dochkrshp  42128  hgmapval0  42634  rrx2pnecoorneor  49462