Theorem necon3ad 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  necon1ad  2958  necon3d  2962  disjpss  4461  2f1fvneq  7259  oeeulem  8601  enp1iOLD  9280  canthp1lem2  10648  winalim2  10691  nlt1pi  10901  sqreulem  15306  rpnnen2lem11  16167  eucalglt  16522  nprm  16625  pcprmpw2  16815  pcmpt  16825  expnprm  16835  prmlem0  17039  pltnle  18291  psgnunilem1  19361  pgpfi  19473  frgpnabllem1  19741  gsumval3a  19771  ablfac1eulem  19942  pgpfaclem2  19952  ablsimpgfindlem1  19977  lspdisjb  20739  lspdisj2  20740  obselocv  21283  mhpmulcl  21692  0nnei  22616  t0dist  22829  t1sep  22874  ordthauslem  22887  hausflim  23485  bcthlem5  24845  bcth  24846  fta1g  25685  plyco0  25706  dgrnznn  25761  coeaddlem  25763  fta1  25821  vieta1lem2  25824  logcnlem3  26152  dvloglem  26156  dcubic  26351  mumullem2  26684  2sqlem8a  26928  dchrisum0flblem1  27011  colperpexlem2  27982  elntg2  28243  1loopgrnb0  28759  usgr2trlncrct  29060  ocnel  30551  hatomistici  31615  lbslsat  32701  sibfof  33339  outsideofrflx  35099  poimirlem23  36511  mblfinlem1  36525  cntotbnd  36664  heiborlem6  36684  lshpnel  37853  lshpcmp  37858  lfl1  37940  lkrshp  37975  lkrpssN  38033  atnlt  38183  atnle  38187  atlatmstc  38189  intnatN  38278  atbtwn  38317  llnnlt  38394  lplnnlt  38436  2llnjaN  38437  lvolnltN  38489  2lplnja  38490  dalem-cly  38542  dalem44  38587  2llnma3r  38659  cdlemblem  38664  lhpm0atN  38900  lhp2atnle  38904  cdlemednpq  39170  cdleme22cN  39213  cdlemg18b  39550  cdlemg42  39600  dia2dimlem1  39935  dochkrshp  40257  hgmapval0  40763  rrx2pnecoorneor  47401