Theorem necon3ad 2959

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon1ad  2963  necon3d  2967  disjpss  4484  2f1fvneq  7297  oeeulem  8657  enp1iOLD  9342  canthp1lem2  10722  winalim2  10765  nlt1pi  10975  sqreulem  15408  rpnnen2lem11  16272  eucalglt  16632  nprm  16735  pcprmpw2  16929  pcmpt  16939  expnprm  16949  prmlem0  17153  pltnle  18408  psgnunilem1  19535  pgpfi  19647  frgpnabllem1  19915  gsumval3a  19945  ablfac1eulem  20116  pgpfaclem2  20126  ablsimpgfindlem1  20151  lspdisjb  21151  lspdisj2  21152  obselocv  21771  mhpmulcl  22176  0nnei  23141  t0dist  23354  t1sep  23399  ordthauslem  23412  hausflim  24010  bcthlem5  25381  bcth  25382  fta1g  26229  plyco0  26251  dgrnznn  26306  coeaddlem  26308  fta1  26368  vieta1lem2  26371  logcnlem3  26704  dvloglem  26708  dcubic  26907  mumullem2  27241  2sqlem8a  27487  dchrisum0flblem1  27570  colperpexlem2  28757  elntg2  29018  1loopgrnb0  29538  usgr2trlncrct  29839  ocnel  31330  hatomistici  32394  1arithufdlem4  33540  lbslsat  33629  sibfof  34305  outsideofrflx  36091  poimirlem23  37603  mblfinlem1  37617  cntotbnd  37756  heiborlem6  37776  lshpnel  38939  lshpcmp  38944  lfl1  39026  lkrshp  39061  lkrpssN  39119  atnlt  39269  atnle  39273  atlatmstc  39275  intnatN  39364  atbtwn  39403  llnnlt  39480  lplnnlt  39522  2llnjaN  39523  lvolnltN  39575  2lplnja  39576  dalem-cly  39628  dalem44  39673  2llnma3r  39745  cdlemblem  39750  lhpm0atN  39986  lhp2atnle  39990  cdlemednpq  40256  cdleme22cN  40299  cdlemg18b  40636  cdlemg42  40686  dia2dimlem1  41021  dochkrshp  41343  hgmapval0  41849  rrx2pnecoorneor  48449