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

Theorem pm2.61dne 2867
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
pm2.61dne.1 (𝜑 → (𝐴 = 𝐵𝜓))
pm2.61dne.2 (𝜑 → (𝐴𝐵𝜓))
Assertion
Ref Expression
pm2.61dne (𝜑𝜓)

Proof of Theorem pm2.61dne
StepHypRef Expression
1 pm2.61dne.2 . 2 (𝜑 → (𝐴𝐵𝜓))
2 nne 2785 . . 3 𝐴𝐵𝐴 = 𝐵)
3 pm2.61dne.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
42, 3syl5bi 230 . 2 (𝜑 → (¬ 𝐴𝐵𝜓))
51, 4pm2.61d 168 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2779
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 195  df-ne 2781
This theorem is referenced by:  pm2.61dane  2868  wefrc  5022  wereu2  5025  oe0lem  7457  fisupg  8070  marypha1lem  8199  fiinfg  8265  wdomtr  8340  unxpwdom2  8353  fpwwe2lem13  9320  grur1a  9497  grutsk  9500  fimaxre2  10818  xlesubadd  11922  cshwidxmod  13346  sqreu  13894  pcxcl  15349  pcmpt  15380  symggen  17659  isabvd  18589  lspprat  18920  mdetralt  20175  ordtrest2lem  20759  ordthauslem  20939  comppfsc  21087  fbssint  21394  fclscf  21581  tgptsmscld  21706  ovoliunnul  22999  itg11  23181  i1fadd  23185  fta1g  23648  plydiveu  23774  fta1  23784  mulcxp  24148  cxpsqrt  24166  ostth3  25044  brbtwn2  25503  colinearalg  25508  clwwisshclww  26101  ordtrest2NEWlem  29102  subfacp1lem5  30226  frmin  30789  btwnexch2  31106  fnemeet2  31338  fnejoin2  31340  limsucncmpi  31420  areacirc  32471  sstotbnd2  32539  ssbnd  32553  prdsbnd2  32560  rrncmslem  32597  atnlt  33414  atlelt  33538  llnnlt  33623  lplnnlt  33665  lvolnltN  33718  pmapglb2N  33871  pmapglb2xN  33872  paddasslem14  33933  cdleme27a  34469  iccpartigtl  39759  clwwisshclwws  41230
  Copyright terms: Public domain W3C validator