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 3100
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 3017 . . 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 3013
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 3014
This theorem is referenced by:  pm2.61dane  3101  wefrc  5542  wereu2  5545  oe0lem  8127  fisupg  8754  marypha1lem  8885  fiinfg  8951  wdomtr  9027  unxpwdom2  9040  fpwwe2lem13  10052  grur1a  10229  grutsk  10232  fimaxre2  11574  xlesubadd  12644  cshwidxmod  14153  sqreu  14708  pcxcl  16185  pcmpt  16216  symggen  18527  isabvd  19520  lspprat  19854  mdetralt  21145  ordtrest2lem  21739  ordthauslem  21919  comppfsc  22068  fbssint  22374  fclscf  22561  tgptsmscld  22686  ovoliunnul  24035  itg11  24219  i1fadd  24223  fta1g  24688  plydiveu  24814  fta1  24824  mulcxp  25195  cxpsqrt  25213  ostth3  26141  brbtwn2  26618  colinearalg  26623  clwwisshclwws  27720  ordtrest2NEWlem  31064  subfacp1lem5  32328  frpomin  32975  frmin  32981  btwnexch2  33381  fnemeet2  33612  fnejoin2  33614  limsucncmpi  33690  areacirc  34868  sstotbnd2  34933  ssbnd  34947  prdsbnd2  34954  rrncmslem  34991  atnlt  36329  atlelt  36454  llnnlt  36539  lplnnlt  36581  lvolnltN  36634  pmapglb2N  36787  pmapglb2xN  36788  paddasslem14  36849  cdleme27a  37383  iccpartigtl  43460
  Copyright terms: Public domain W3C validator