Theorem necon3ad 2938

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon1ad  2942  necon3d  2946  disjpss  4424  oeeulem  8565  enp1iOLD  9225  canthp1lem2  10606  winalim2  10649  nlt1pi  10859  sqreulem  15326  rpnnen2lem11  16192  eucalglt  16555  nprm  16658  pcprmpw2  16853  pcmpt  16863  expnprm  16873  prmlem0  17076  pltnle  18297  psgnunilem1  19423  pgpfi  19535  frgpnabllem1  19803  gsumval3a  19833  ablfac1eulem  20004  pgpfaclem2  20014  ablsimpgfindlem1  20039  lspdisjb  21036  lspdisj2  21037  obselocv  21637  mhpmulcl  22036  0nnei  22999  t0dist  23212  t1sep  23257  ordthauslem  23270  hausflim  23868  bcthlem5  25228  bcth  25229  fta1g  26075  plyco0  26097  dgrnznn  26152  coeaddlem  26154  fta1  26216  vieta1lem2  26219  logcnlem3  26553  dvloglem  26557  dcubic  26756  mumullem2  27090  2sqlem8a  27336  dchrisum0flblem1  27419  colperpexlem2  28658  elntg2  28912  1loopgrnb0  29430  usgr2trlncrct  29736  ocnel  31227  hatomistici  32291  1arithufdlem4  33518  lbslsat  33612  sibfof  34331  outsideofrflx  36115  poimirlem23  37637  mblfinlem1  37651  cntotbnd  37790  heiborlem6  37810  lshpnel  38976  lshpcmp  38981  lfl1  39063  lkrshp  39098  lkrpssN  39156  atnlt  39306  atnle  39310  atlatmstc  39312  intnatN  39401  atbtwn  39440  llnnlt  39517  lplnnlt  39559  2llnjaN  39560  lvolnltN  39612  2lplnja  39613  dalem-cly  39665  dalem44  39710  2llnma3r  39782  cdlemblem  39787  lhpm0atN  40023  lhp2atnle  40027  cdlemednpq  40293  cdleme22cN  40336  cdlemg18b  40673  cdlemg42  40723  dia2dimlem1  41058  dochkrshp  41380  hgmapval0  41886  rrx2pnecoorneor  48704