Theorem necon3ad 2982

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1601   ≠ wne 2969

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 199  df-ne 2970

This theorem is referenced by:  necon1ad  2986  necon3d  2990  disjpss  4253  2f1fvneq  6789  oeeulem  7965  enp1i  8483  canthp1lem2  9810  winalim2  9853  nlt1pi  10063  sqreulem  14506  rpnnen2lem11  15357  eucalglt  15704  nprm  15806  pcprmpw2  15990  pcmpt  16000  expnprm  16010  prmlem0  16211  pltnle  17352  psgnunilem1  18296  pgpfi  18404  frgpnabllem1  18662  gsumval3a  18690  ablfac1eulem  18858  pgpfaclem2  18868  lspdisjb  19521  lspdisj2  19522  obselocv  20471  0nnei  21324  t0dist  21537  t1sep  21582  ordthauslem  21595  hausflim  22193  bcthlem5  23534  bcth  23535  fta1g  24364  plyco0  24385  dgrnznn  24440  coeaddlem  24442  fta1  24500  vieta1lem2  24503  logcnlem3  24827  dvloglem  24831  dcubic  25024  mumullem2  25358  2sqlem8a  25602  dchrisum0flblem1  25649  colperpexlem2  26079  elntg2  26334  1loopgrnb0  26850  usgr2trlncrct  27155  ocnel  28729  hatomistici  29793  lbslsat  30432  sibfof  31000  outsideofrflx  32823  poimirlem23  34058  mblfinlem1  34072  cntotbnd  34219  heiborlem6  34239  lshpnel  35137  lshpcmp  35142  lfl1  35224  lkrshp  35259  lkrpssN  35317  atnlt  35467  atnle  35471  atlatmstc  35473  intnatN  35561  atbtwn  35600  llnnlt  35677  lplnnlt  35719  2llnjaN  35720  lvolnltN  35772  2lplnja  35773  dalem-cly  35825  dalem44  35870  2llnma3r  35942  cdlemblem  35947  lhpm0atN  36183  lhp2atnle  36187  cdlemednpq  36453  cdleme22cN  36496  cdlemg18b  36833  cdlemg42  36883  dia2dimlem1  37218  dochkrshp  37540  hgmapval0  38046  rrx2pnecoorneor  43451