Theorem necon3ad 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2941

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 206  df-ne 2942

This theorem is referenced by:  necon1ad  2958  necon3d  2962  disjpss  4418  2f1fvneq  7203  oeeulem  8540  enp1iOLD  9182  canthp1lem2  10547  winalim2  10590  nlt1pi  10800  sqreulem  15204  rpnnen2lem11  16066  eucalglt  16421  nprm  16524  pcprmpw2  16714  pcmpt  16724  expnprm  16734  prmlem0  16938  pltnle  18187  psgnunilem1  19234  pgpfi  19346  frgpnabllem1  19610  gsumval3a  19639  ablfac1eulem  19810  pgpfaclem2  19820  ablsimpgfindlem1  19845  lspdisjb  20540  lspdisj2  20541  obselocv  21087  mhpmulcl  21491  0nnei  22415  t0dist  22628  t1sep  22673  ordthauslem  22686  hausflim  23284  bcthlem5  24644  bcth  24645  fta1g  25484  plyco0  25505  dgrnznn  25560  coeaddlem  25562  fta1  25620  vieta1lem2  25623  logcnlem3  25951  dvloglem  25955  dcubic  26148  mumullem2  26481  2sqlem8a  26725  dchrisum0flblem1  26808  colperpexlem2  27502  elntg2  27763  1loopgrnb0  28279  usgr2trlncrct  28580  ocnel  30069  hatomistici  31133  lbslsat  32133  sibfof  32752  outsideofrflx  34650  poimirlem23  36039  mblfinlem1  36053  cntotbnd  36193  heiborlem6  36213  lshpnel  37383  lshpcmp  37388  lfl1  37470  lkrshp  37505  lkrpssN  37563  atnlt  37713  atnle  37717  atlatmstc  37719  intnatN  37808  atbtwn  37847  llnnlt  37924  lplnnlt  37966  2llnjaN  37967  lvolnltN  38019  2lplnja  38020  dalem-cly  38072  dalem44  38117  2llnma3r  38189  cdlemblem  38194  lhpm0atN  38430  lhp2atnle  38434  cdlemednpq  38700  cdleme22cN  38743  cdlemg18b  39080  cdlemg42  39130  dia2dimlem1  39465  dochkrshp  39787  hgmapval0  40293  rrx2pnecoorneor  46702