Theorem necon1bd 2951

Description: Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

Hypothesis

Ref	Expression
necon1bd.1	⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))

Assertion

Ref	Expression
necon1bd	⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

Proof of Theorem necon1bd

Step	Hyp	Ref	Expression
1		df-ne 2934	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bd.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
3	1, 2	biimtrrid 243	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓))
4	3	con1d 145	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

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

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 2934

This theorem is referenced by:  necon4ad  2952  fvclss  7187  suppssr  8136  suppssrg  8137  suppofssd  8144  eceqoveq  8760  fofinf1o  9233  cantnfp1lem3  9590  cantnfp1  9591  mul0or  11778  rimul  12137  rlimuni  15474  pc2dvds  16808  divsfval  17469  pleval2i  18258  lssvs0or  21067  lspsnat  21102  psdmul  22110  lmmo  23323  filssufilg  23854  hausflimi  23923  fclscf  23968  xrsmopn  24756  rectbntr0  24776  bcth3  25276  limcco  25838  ig1pdvds  26126  plyco0  26138  plypf1  26158  coeeulem  26170  coeidlem  26183  coeid3  26186  coemullem  26196  coemulhi  26200  coemulc  26201  dgradd2  26214  vieta1lem2  26259  dvtaylp  26318  musum  27141  perfectlem2  27181  dchrelbas3  27189  dchrmullid  27203  dchreq  27209  dchrsum  27220  gausslemma2dlem4  27320  dchrisum0re  27464  muls0ord  28165  coltr  28703  lmieu  28840  pthisspthorcycl  29859  elspansn5  31634  atomli  32442  onsucconni  36625  poimirlem8  37940  poimirlem9  37941  poimirlem18  37950  poimirlem21  37953  poimirlem22  37954  poimirlem26  37958  lshpcmp  39425  lsator0sp  39438  atnle  39754  atlatmstc  39756  osumcllem8N  40400  osumcllem11N  40403  pexmidlem5N  40411  pexmidlem8N  40414  dochsat0  41894  dochexmidlem5  41901  dochexmidlem8  41904  aks6d1c4  42555  sn-remul0ord  42839  fsuppind  43022  congabseq  43405  dflim5  43760  mnringmulrcld  44658  perfectALTVlem2  48156