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 3103
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 3020 . . 3 𝐴𝐵𝐴 = 𝐵)
3 pm2.61dne.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
42, 3syl5bi 243 . 2 (𝜑 → (¬ 𝐴𝐵𝜓))
51, 4pm2.61d 180 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 3017
This theorem is referenced by:  pm2.61dane  3104  wefrc  5543  wereu2  5546  oe0lem  8129  fisupg  8755  marypha1lem  8886  fiinfg  8952  wdomtr  9028  unxpwdom2  9041  fpwwe2lem13  10053  grur1a  10230  grutsk  10233  fimaxre2  11575  xlesubadd  12646  cshwidxmod  14155  sqreu  14710  pcxcl  16187  pcmpt  16218  symggen  18529  isabvd  19522  lspprat  19856  mdetralt  21147  ordtrest2lem  21741  ordthauslem  21921  comppfsc  22070  fbssint  22376  fclscf  22563  tgptsmscld  22688  ovoliunnul  24037  itg11  24221  i1fadd  24225  fta1g  24690  plydiveu  24816  fta1  24826  mulcxp  25195  cxpsqrt  25213  ostth3  26142  brbtwn2  26619  colinearalg  26624  clwwisshclwws  27721  ordtrest2NEWlem  31065  subfacp1lem5  32329  frpomin  32976  frmin  32982  btwnexch2  33382  fnemeet2  33613  fnejoin2  33615  limsucncmpi  33691  areacirc  34869  sstotbnd2  34935  ssbnd  34949  prdsbnd2  34956  rrncmslem  34993  atnlt  36331  atlelt  36456  llnnlt  36541  lplnnlt  36583  lvolnltN  36636  pmapglb2N  36789  pmapglb2xN  36790  paddasslem14  36851  cdleme27a  37385  iccpartigtl  43430
  Copyright terms: Public domain W3C validator