Theorem necon3ad 3029

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

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

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 209  df-ne 3017

This theorem is referenced by:  necon1ad  3033  necon3d  3037  disjpss  4409  2f1fvneq  7017  oeeulem  8226  enp1i  8752  canthp1lem2  10074  winalim2  10117  nlt1pi  10327  sqreulem  14718  rpnnen2lem11  15576  eucalglt  15928  nprm  16031  pcprmpw2  16217  pcmpt  16227  expnprm  16237  prmlem0  16438  pltnle  17575  psgnunilem1  18620  pgpfi  18729  frgpnabllem1  18992  gsumval3a  19022  ablfac1eulem  19193  pgpfaclem2  19203  ablsimpgfindlem1  19228  lspdisjb  19897  lspdisj2  19898  obselocv  20871  0nnei  21719  t0dist  21932  t1sep  21977  ordthauslem  21990  hausflim  22588  bcthlem5  23930  bcth  23931  fta1g  24760  plyco0  24781  dgrnznn  24836  coeaddlem  24838  fta1  24896  vieta1lem2  24899  logcnlem3  25226  dvloglem  25230  dcubic  25423  mumullem2  25756  2sqlem8a  26000  dchrisum0flblem1  26083  colperpexlem2  26516  elntg2  26770  1loopgrnb0  27283  usgr2trlncrct  27583  ocnel  29074  hatomistici  30138  lbslsat  31014  sibfof  31598  outsideofrflx  33588  poimirlem23  34914  mblfinlem1  34928  cntotbnd  35073  heiborlem6  35093  lshpnel  36118  lshpcmp  36123  lfl1  36205  lkrshp  36240  lkrpssN  36298  atnlt  36448  atnle  36452  atlatmstc  36454  intnatN  36542  atbtwn  36581  llnnlt  36658  lplnnlt  36700  2llnjaN  36701  lvolnltN  36753  2lplnja  36754  dalem-cly  36806  dalem44  36851  2llnma3r  36923  cdlemblem  36928  lhpm0atN  37164  lhp2atnle  37168  cdlemednpq  37434  cdleme22cN  37477  cdlemg18b  37814  cdlemg42  37864  dia2dimlem1  38199  dochkrshp  38521  hgmapval0  39027  rrx2pnecoorneor  44701