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  7189  suppssr  8138  suppssrg  8139  suppofssd  8146  eceqoveq  8762  fofinf1o  9235  cantnfp1lem3  9592  cantnfp1  9593  mul0or  11781  rimul  12141  rlimuni  15503  pc2dvds  16841  divsfval  17502  pleval2i  18291  lssvs0or  21100  lspsnat  21135  psdmul  22142  lmmo  23355  filssufilg  23886  hausflimi  23955  fclscf  24000  xrsmopn  24788  rectbntr0  24808  bcth3  25308  limcco  25870  ig1pdvds  26155  plyco0  26167  plypf1  26187  coeeulem  26199  coeidlem  26212  coeid3  26215  coemullem  26225  coemulhi  26229  coemulc  26230  dgradd2  26243  vieta1lem2  26288  dvtaylp  26347  musum  27168  perfectlem2  27207  dchrelbas3  27215  dchrmullid  27229  dchreq  27235  dchrsum  27246  gausslemma2dlem4  27346  dchrisum0re  27490  muls0ord  28191  coltr  28729  lmieu  28866  pthisspthorcycl  29885  elspansn5  31660  atomli  32468  onsucconni  36635  poimirlem8  37963  poimirlem9  37964  poimirlem18  37973  poimirlem21  37976  poimirlem22  37977  poimirlem26  37981  lshpcmp  39448  lsator0sp  39461  atnle  39777  atlatmstc  39779  osumcllem8N  40423  osumcllem11N  40426  pexmidlem5N  40434  pexmidlem8N  40437  dochsat0  41917  dochexmidlem5  41924  dochexmidlem8  41927  aks6d1c4  42577  sn-remul0ord  42854  fsuppind  43037  congabseq  43420  dflim5  43775  mnringmulrcld  44673  perfectALTVlem2  48210