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 1541   ≠ 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  4409  oeeulem  8511  canthp1lem2  10536  winalim2  10579  nlt1pi  10789  sqreulem  15259  rpnnen2lem11  16125  eucalglt  16488  nprm  16591  pcprmpw2  16786  pcmpt  16796  expnprm  16806  prmlem0  17009  pltnle  18234  psgnunilem1  19398  pgpfi  19510  frgpnabllem1  19778  gsumval3a  19808  ablfac1eulem  19979  pgpfaclem2  19989  ablsimpgfindlem1  20014  lspdisjb  21056  lspdisj2  21057  obselocv  21658  mhpmulcl  22057  0nnei  23020  t0dist  23233  t1sep  23278  ordthauslem  23291  hausflim  23889  bcthlem5  25248  bcth  25249  fta1g  26095  plyco0  26117  dgrnznn  26172  coeaddlem  26174  fta1  26236  vieta1lem2  26239  logcnlem3  26573  dvloglem  26577  dcubic  26776  mumullem2  27110  2sqlem8a  27356  dchrisum0flblem1  27439  colperpexlem2  28702  elntg2  28956  1loopgrnb0  29474  usgr2trlncrct  29777  ocnel  31268  hatomistici  32332  1arithufdlem4  33502  lbslsat  33619  sibfof  34343  outsideofrflx  36140  poimirlem23  37662  mblfinlem1  37676  cntotbnd  37815  heiborlem6  37835  lshpnel  39001  lshpcmp  39006  lfl1  39088  lkrshp  39123  lkrpssN  39181  atnlt  39331  atnle  39335  atlatmstc  39337  intnatN  39425  atbtwn  39464  llnnlt  39541  lplnnlt  39583  2llnjaN  39584  lvolnltN  39636  2lplnja  39637  dalem-cly  39689  dalem44  39734  2llnma3r  39806  cdlemblem  39811  lhpm0atN  40047  lhp2atnle  40051  cdlemednpq  40317  cdleme22cN  40360  cdlemg18b  40697  cdlemg42  40747  dia2dimlem1  41082  dochkrshp  41404  hgmapval0  41910  rrx2pnecoorneor  48726