Theorem necon3ad 2939

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2926

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 2927

This theorem is referenced by:  necon1ad  2943  necon3d  2947  disjpss  4427  oeeulem  8568  enp1iOLD  9232  canthp1lem2  10613  winalim2  10656  nlt1pi  10866  sqreulem  15333  rpnnen2lem11  16199  eucalglt  16562  nprm  16665  pcprmpw2  16860  pcmpt  16870  expnprm  16880  prmlem0  17083  pltnle  18304  psgnunilem1  19430  pgpfi  19542  frgpnabllem1  19810  gsumval3a  19840  ablfac1eulem  20011  pgpfaclem2  20021  ablsimpgfindlem1  20046  lspdisjb  21043  lspdisj2  21044  obselocv  21644  mhpmulcl  22043  0nnei  23006  t0dist  23219  t1sep  23264  ordthauslem  23277  hausflim  23875  bcthlem5  25235  bcth  25236  fta1g  26082  plyco0  26104  dgrnznn  26159  coeaddlem  26161  fta1  26223  vieta1lem2  26226  logcnlem3  26560  dvloglem  26564  dcubic  26763  mumullem2  27097  2sqlem8a  27343  dchrisum0flblem1  27426  colperpexlem2  28665  elntg2  28919  1loopgrnb0  29437  usgr2trlncrct  29743  ocnel  31234  hatomistici  32298  1arithufdlem4  33525  lbslsat  33619  sibfof  34338  outsideofrflx  36122  poimirlem23  37644  mblfinlem1  37658  cntotbnd  37797  heiborlem6  37817  lshpnel  38983  lshpcmp  38988  lfl1  39070  lkrshp  39105  lkrpssN  39163  atnlt  39313  atnle  39317  atlatmstc  39319  intnatN  39408  atbtwn  39447  llnnlt  39524  lplnnlt  39566  2llnjaN  39567  lvolnltN  39619  2lplnja  39620  dalem-cly  39672  dalem44  39717  2llnma3r  39789  cdlemblem  39794  lhpm0atN  40030  lhp2atnle  40034  cdlemednpq  40300  cdleme22cN  40343  cdlemg18b  40680  cdlemg42  40730  dia2dimlem1  41065  dochkrshp  41387  hgmapval0  41893  rrx2pnecoorneor  48708