Theorem necon3ad 2943

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 2930

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 2931

This theorem is referenced by:  necon1ad  2947  necon3d  2951  disjpss  4461  2f1fvneq  7268  oeeulem  8620  enp1iOLD  9303  canthp1lem2  10676  winalim2  10719  nlt1pi  10929  sqreulem  15338  rpnnen2lem11  16200  eucalglt  16555  nprm  16658  pcprmpw2  16850  pcmpt  16860  expnprm  16870  prmlem0  17074  pltnle  18329  psgnunilem1  19452  pgpfi  19564  frgpnabllem1  19832  gsumval3a  19862  ablfac1eulem  20033  pgpfaclem2  20043  ablsimpgfindlem1  20068  lspdisjb  21018  lspdisj2  21019  obselocv  21666  mhpmulcl  22081  0nnei  23046  t0dist  23259  t1sep  23304  ordthauslem  23317  hausflim  23915  bcthlem5  25286  bcth  25287  fta1g  26134  plyco0  26156  dgrnznn  26211  coeaddlem  26213  fta1  26273  vieta1lem2  26276  logcnlem3  26608  dvloglem  26612  dcubic  26808  mumullem2  27142  2sqlem8a  27388  dchrisum0flblem1  27471  colperpexlem2  28591  elntg2  28852  1loopgrnb0  29372  usgr2trlncrct  29673  ocnel  31164  hatomistici  32228  lbslsat  33384  sibfof  34030  outsideofrflx  35793  poimirlem23  37186  mblfinlem1  37200  cntotbnd  37339  heiborlem6  37359  lshpnel  38524  lshpcmp  38529  lfl1  38611  lkrshp  38646  lkrpssN  38704  atnlt  38854  atnle  38858  atlatmstc  38860  intnatN  38949  atbtwn  38988  llnnlt  39065  lplnnlt  39107  2llnjaN  39108  lvolnltN  39160  2lplnja  39161  dalem-cly  39213  dalem44  39258  2llnma3r  39330  cdlemblem  39335  lhpm0atN  39571  lhp2atnle  39575  cdlemednpq  39841  cdleme22cN  39884  cdlemg18b  40221  cdlemg42  40271  dia2dimlem1  40606  dochkrshp  40928  hgmapval0  41434  rrx2pnecoorneor  47900