Theorem necon3ad 2807

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ≠ wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necon1ad  2811  necon3d  2815  disjpss  4028  2f1fvneq  6517  oeeulem  7681  enp1i  8195  canthp1lem2  9475  winalim2  9518  nlt1pi  9728  sqreulem  14099  rpnnen2lem11  14953  eucalglt  15298  nprm  15401  pcprmpw2  15586  pcmpt  15596  expnprm  15606  prmlem0  15812  pltnle  16966  psgnunilem1  17913  pgpfi  18020  frgpnabllem1  18276  gsumval3a  18304  ablfac1eulem  18471  pgpfaclem2  18481  lspdisjb  19126  lspdisj2  19127  obselocv  20072  0nnei  20916  t0dist  21129  t1sep  21174  ordthauslem  21187  hausflim  21785  bcthlem5  23125  bcth  23126  fta1g  23927  plyco0  23948  dgrnznn  24003  coeaddlem  24005  fta1  24063  vieta1lem2  24066  logcnlem3  24390  dvloglem  24394  dcubic  24573  mumullem2  24906  2sqlem8a  25150  dchrisum0flblem1  25197  colperpexlem2  25623  1loopgrnb0  26398  usgr2trlncrct  26698  ocnel  28157  hatomistici  29221  sibfof  30402  outsideofrflx  32234  poimirlem23  33432  mblfinlem1  33446  cntotbnd  33595  heiborlem6  33615  lshpnel  34270  lshpcmp  34275  lfl1  34357  lkrshp  34392  lkrpssN  34450  atnlt  34600  atnle  34604  atlatmstc  34606  intnatN  34693  atbtwn  34732  llnnlt  34809  lplnnlt  34851  2llnjaN  34852  lvolnltN  34904  2lplnja  34905  dalem-cly  34957  dalem44  35002  2llnma3r  35074  cdlemblem  35079  lhpm0atN  35315  lhp2atnle  35319  cdlemednpq  35586  cdleme22cN  35630  cdlemg18b  35967  cdlemg42  36017  dia2dimlem1  36353  dochkrshp  36675  hgmapval0  37184