MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon1bd Structured version   Visualization version   GIF version

Theorem necon1bd 3038
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
StepHypRef Expression
1 df-ne 3021 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon1bd.1 . . 3 (𝜑 → (𝐴𝐵𝜓))
31, 2syl5bir 244 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝜓))
43con1d 147 1 (𝜑 → (¬ 𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1530  wne 3020
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 208  df-ne 3021
This theorem is referenced by:  necon4ad  3039  fvclss  6998  suppssr  7855  suppofssd  7861  eceqoveq  8395  fofinf1o  8791  cantnfp1lem3  9135  cantnfp1  9136  mul0or  11272  inelr  11620  rimul  11621  rlimuni  14900  pc2dvds  16207  divsfval  16812  pleval2i  17566  lssvs0or  19804  lspsnat  19839  lmmo  21904  filssufilg  22435  hausflimi  22504  fclscf  22549  xrsmopn  23335  rectbntr0  23355  bcth3  23849  limcco  24406  ig1pdvds  24685  plyco0  24697  plypf1  24717  coeeulem  24729  coeidlem  24742  coeid3  24745  coemullem  24755  coemulhi  24759  coemulc  24760  dgradd2  24773  vieta1lem2  24815  dvtaylp  24873  musum  25682  perfectlem2  25720  dchrelbas3  25728  dchrmulid2  25742  dchreq  25748  dchrsum  25759  gausslemma2dlem4  25859  dchrisum0re  26003  coltr  26347  lmieu  26484  elspansn5  29266  atomli  30074  pthisspthorcycl  32260  onsucconni  33670  poimirlem8  34768  poimirlem9  34769  poimirlem18  34778  poimirlem21  34781  poimirlem22  34782  poimirlem26  34786  lshpcmp  35992  lsator0sp  36005  atnle  36321  atlatmstc  36323  osumcllem8N  36967  osumcllem11N  36970  pexmidlem5N  36978  pexmidlem8N  36981  dochsat0  38461  dochexmidlem5  38468  dochexmidlem8  38471  congabseq  39433  perfectALTVlem2  43716
  Copyright terms: Public domain W3C validator