Theorem necon3ad 2970

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

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

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 2958

This theorem is used by:  necon1ad  2974  necon3d  2978  disjpss  4420  oeeulem  8585  canthp1lem2  10644  winalim2  10687  nlt1pi  10897  sqreulem  15418  rpnnen2lem11  16286  eucalglt  16649  nprm  16752  pcprmpw2  16948  pcmpt  16958  expnprm  16968  prmlem0  17171  pltnle  18398  psgnunilem1  19569  pgpfi  19681  frgpnabllem1  19949  gsumval3a  19979  ablfac1eulem  20150  pgpfaclem2  20160  ablsimpgfindlem1  20185  lspdisjb  21261  lspdisj2  21262  obselocv  21889  mhpmulcl  22323  0nnei  23280  t0dist  23493  t1sep  23538  ordthauslem  23551  hausflim  24149  bcthlem5  25498  bcth  25499  fta1g  26338  plyco0  26360  dgrnznn  26415  coeaddlem  26417  fta1  26480  vieta1lem2  26483  logcnlem3  26820  dvloglem  26824  dcubic  27022  mumullem2  27355  2sqlem8a  27600  dchrisum0flblem1  27683  colperpexlem2  29023  elntg2  29346  1loopgrnb0  29863  usgr2trlncrct  30166  ocnel  31661  hatomistici  32725  1arithufdlem4  33846  lbslsat  34015  sibfof  34739  outsideofrflx  36627  poimirlem23  38322  mblfinlem1  38336  cntotbnd  38475  heiborlem6  38495  lshpnel  39785  lshpcmp  39790  lfl1  39872  lkrshp  39907  lkrpssN  39965  atnlt  40115  atnle  40119  atlatmstc  40121  intnatN  40209  atbtwn  40248  llnnlt  40325  lplnnlt  40367  2llnjaN  40368  lvolnltN  40420  2lplnja  40421  dalem-cly  40473  dalem44  40518  2llnma3r  40590  cdlemblem  40595  lhpm0atN  40831  lhp2atnle  40835  cdlemednpq  41101  cdleme22cN  41144  cdlemg18b  41481  cdlemg42  41531  dia2dimlem1  41866  dochkrshp  42188  hgmapval0  42694  rrx2pnecoorneor  49523