Theorem necon3ad 2943

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2930

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 2931

This theorem is referenced by:  necon1ad  2947  necon3d  2951  disjpss  4412  oeeulem  8525  canthp1lem2  10554  winalim2  10597  nlt1pi  10807  sqreulem  15277  rpnnen2lem11  16143  eucalglt  16506  nprm  16609  pcprmpw2  16804  pcmpt  16814  expnprm  16824  prmlem0  17027  pltnle  18252  psgnunilem1  19415  pgpfi  19527  frgpnabllem1  19795  gsumval3a  19825  ablfac1eulem  19996  pgpfaclem2  20006  ablsimpgfindlem1  20031  lspdisjb  21073  lspdisj2  21074  obselocv  21675  mhpmulcl  22074  0nnei  23037  t0dist  23250  t1sep  23295  ordthauslem  23308  hausflim  23906  bcthlem5  25265  bcth  25266  fta1g  26112  plyco0  26134  dgrnznn  26189  coeaddlem  26191  fta1  26253  vieta1lem2  26256  logcnlem3  26590  dvloglem  26594  dcubic  26793  mumullem2  27127  2sqlem8a  27373  dchrisum0flblem1  27456  colperpexlem2  28719  elntg2  28974  1loopgrnb0  29492  usgr2trlncrct  29795  ocnel  31289  hatomistici  32353  1arithufdlem4  33523  lbslsat  33640  sibfof  34364  outsideofrflx  36182  poimirlem23  37693  mblfinlem1  37707  cntotbnd  37846  heiborlem6  37866  lshpnel  39092  lshpcmp  39097  lfl1  39179  lkrshp  39214  lkrpssN  39272  atnlt  39422  atnle  39426  atlatmstc  39428  intnatN  39516  atbtwn  39555  llnnlt  39632  lplnnlt  39674  2llnjaN  39675  lvolnltN  39727  2lplnja  39728  dalem-cly  39780  dalem44  39825  2llnma3r  39897  cdlemblem  39902  lhpm0atN  40138  lhp2atnle  40142  cdlemednpq  40408  cdleme22cN  40451  cdlemg18b  40788  cdlemg42  40838  dia2dimlem1  41173  dochkrshp  41495  hgmapval0  42001  rrx2pnecoorneor  48830