Theorem necon3ad 2957

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

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

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 2945

This theorem is referenced by:  necon1ad  2961  necon3d  2965  disjpss  4395  2f1fvneq  7142  oeeulem  8441  enp1i  9061  canthp1lem2  10418  winalim2  10461  nlt1pi  10671  sqreulem  15080  rpnnen2lem11  15942  eucalglt  16299  nprm  16402  pcprmpw2  16592  pcmpt  16602  expnprm  16612  prmlem0  16816  pltnle  18065  psgnunilem1  19110  pgpfi  19219  frgpnabllem1  19483  gsumval3a  19513  ablfac1eulem  19684  pgpfaclem2  19694  ablsimpgfindlem1  19719  lspdisjb  20397  lspdisj2  20398  obselocv  20944  mhpmulcl  21348  0nnei  22272  t0dist  22485  t1sep  22530  ordthauslem  22543  hausflim  23141  bcthlem5  24501  bcth  24502  fta1g  25341  plyco0  25362  dgrnznn  25417  coeaddlem  25419  fta1  25477  vieta1lem2  25480  logcnlem3  25808  dvloglem  25812  dcubic  26005  mumullem2  26338  2sqlem8a  26582  dchrisum0flblem1  26665  colperpexlem2  27101  elntg2  27362  1loopgrnb0  27878  usgr2trlncrct  28180  ocnel  29669  hatomistici  30733  lbslsat  31708  sibfof  32316  outsideofrflx  34438  poimirlem23  35809  mblfinlem1  35823  cntotbnd  35963  heiborlem6  35983  lshpnel  37004  lshpcmp  37009  lfl1  37091  lkrshp  37126  lkrpssN  37184  atnlt  37334  atnle  37338  atlatmstc  37340  intnatN  37428  atbtwn  37467  llnnlt  37544  lplnnlt  37586  2llnjaN  37587  lvolnltN  37639  2lplnja  37640  dalem-cly  37692  dalem44  37737  2llnma3r  37809  cdlemblem  37814  lhpm0atN  38050  lhp2atnle  38054  cdlemednpq  38320  cdleme22cN  38363  cdlemg18b  38700  cdlemg42  38750  dia2dimlem1  39085  dochkrshp  39407  hgmapval0  39913  rrx2pnecoorneor  46072