Theorem necon3ad 2951

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2938

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 2939

This theorem is referenced by:  necon1ad  2955  necon3d  2959  disjpss  4459  2f1fvneq  7261  oeeulem  8603  enp1iOLD  9282  canthp1lem2  10650  winalim2  10693  nlt1pi  10903  sqreulem  15310  rpnnen2lem11  16171  eucalglt  16526  nprm  16629  pcprmpw2  16819  pcmpt  16829  expnprm  16839  prmlem0  17043  pltnle  18295  psgnunilem1  19402  pgpfi  19514  frgpnabllem1  19782  gsumval3a  19812  ablfac1eulem  19983  pgpfaclem2  19993  ablsimpgfindlem1  20018  lspdisjb  20884  lspdisj2  20885  obselocv  21502  mhpmulcl  21911  0nnei  22836  t0dist  23049  t1sep  23094  ordthauslem  23107  hausflim  23705  bcthlem5  25076  bcth  25077  fta1g  25920  plyco0  25941  dgrnznn  25996  coeaddlem  25998  fta1  26057  vieta1lem2  26060  logcnlem3  26388  dvloglem  26392  dcubic  26587  mumullem2  26920  2sqlem8a  27164  dchrisum0flblem1  27247  colperpexlem2  28249  elntg2  28510  1loopgrnb0  29026  usgr2trlncrct  29327  ocnel  30818  hatomistici  31882  lbslsat  32989  sibfof  33637  outsideofrflx  35403  poimirlem23  36814  mblfinlem1  36828  cntotbnd  36967  heiborlem6  36987  lshpnel  38156  lshpcmp  38161  lfl1  38243  lkrshp  38278  lkrpssN  38336  atnlt  38486  atnle  38490  atlatmstc  38492  intnatN  38581  atbtwn  38620  llnnlt  38697  lplnnlt  38739  2llnjaN  38740  lvolnltN  38792  2lplnja  38793  dalem-cly  38845  dalem44  38890  2llnma3r  38962  cdlemblem  38967  lhpm0atN  39203  lhp2atnle  39207  cdlemednpq  39473  cdleme22cN  39516  cdlemg18b  39853  cdlemg42  39903  dia2dimlem1  40238  dochkrshp  40560  hgmapval0  41066  rrx2pnecoorneor  47488