Theorem necon3ad 2968

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  necon1ad  2972  necon3d  2976  disjpss  4413  oeeulem  8588  canthp1lem2  10710  winalim2  10753  nlt1pi  10963  sqreulem  15495  rpnnen2lem11  16360  eucalglt  16723  nprm  16826  pcprmpw2  17022  pcmpt  17032  expnprm  17042  prmlem0  17245  pltnle  18472  psgnunilem1  19669  pgpfi  19781  frgpnabllem1  20049  gsumval3a  20079  ablfac1eulem  20250  pgpfaclem2  20260  ablsimpgfindlem1  20285  lspdisjb  21366  lspdisj2  21367  obselocv  21996  mhpmulcl  22432  0nnei  23392  t0dist  23605  t1sep  23650  ordthauslem  23663  hausflim  24262  bcthlem5  25611  bcth  25612  fta1g  26450  plyco0  26472  dgrnznn  26528  coeaddlem  26530  fta1  26593  vieta1lem2  26598  logcnlem3  26936  dvloglem  26940  dcubic  27138  mumullem2  27471  2sqlem8a  27716  dchrisum0flblem1  27799  colperpexlem2  29141  elntg2  29497  1loopgrnb0  30017  usgr2trlncrct  30329  ocnel  31834  hatomistici  32898  1arithufdlem4  34013  lbslsat  34182  sibfof  34907  outsideofrflx  36814  poimirlem23  38481  mblfinlem1  38495  cntotbnd  38650  heiborlem6  38670  lshpnel  39960  lshpcmp  39965  lfl1  40047  lkrshp  40082  lkrpssN  40140  atnlt  40290  atnle  40294  atlatmstc  40296  intnatN  40384  atbtwn  40423  llnnlt  40500  lplnnlt  40542  2llnjaN  40543  lvolnltN  40595  2lplnja  40596  dalem-cly  40648  dalem44  40693  2llnma3r  40765  cdlemblem  40770  lhpm0atN  41006  lhp2atnle  41010  cdlemednpq  41276  cdleme22cN  41319  cdlemg18b  41656  cdlemg42  41706  dia2dimlem1  42041  dochkrshp  42363  hgmapval0  42869  rrx2pnecoorneor  49749