Theorem necon3ad 2948

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necon1ad  2952  necon3d  2956  disjpss  4396  oeeulem  8534  canthp1lem2  10574  winalim2  10617  nlt1pi  10827  sqreulem  15320  rpnnen2lem11  16189  eucalglt  16552  nprm  16655  pcprmpw2  16851  pcmpt  16861  expnprm  16871  prmlem0  17074  pltnle  18300  psgnunilem1  19466  pgpfi  19578  frgpnabllem1  19846  gsumval3a  19876  ablfac1eulem  20047  pgpfaclem2  20057  ablsimpgfindlem1  20082  lspdisjb  21126  lspdisj2  21127  obselocv  21710  mhpmulcl  22144  0nnei  23102  t0dist  23315  t1sep  23360  ordthauslem  23373  hausflim  23971  bcthlem5  25320  bcth  25321  fta1g  26160  plyco0  26182  dgrnznn  26237  coeaddlem  26239  fta1  26299  vieta1lem2  26302  logcnlem3  26633  dvloglem  26637  dcubic  26835  mumullem2  27168  2sqlem8a  27413  dchrisum0flblem1  27496  colperpexlem2  28824  elntg2  29079  1loopgrnb0  29596  usgr2trlncrct  29899  ocnel  31394  hatomistici  32458  1arithufdlem4  33637  lbslsat  33807  sibfof  34531  outsideofrflx  36356  poimirlem23  38011  mblfinlem1  38025  cntotbnd  38164  heiborlem6  38184  lshpnel  39476  lshpcmp  39481  lfl1  39563  lkrshp  39598  lkrpssN  39656  atnlt  39806  atnle  39810  atlatmstc  39812  intnatN  39900  atbtwn  39939  llnnlt  40016  lplnnlt  40058  2llnjaN  40059  lvolnltN  40111  2lplnja  40112  dalem-cly  40164  dalem44  40209  2llnma3r  40281  cdlemblem  40286  lhpm0atN  40522  lhp2atnle  40526  cdlemednpq  40792  cdleme22cN  40835  cdlemg18b  41172  cdlemg42  41222  dia2dimlem1  41557  dochkrshp  41879  hgmapval0  42385  rrx2pnecoorneor  49207