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 3076
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 2994 . . 3 𝐴𝐵𝐴 = 𝐵)
3 pm2.61dne.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
42, 3syl5bi 245 . 2 (𝜑 → (¬ 𝐴𝐵𝜓))
51, 4pm2.61d 182 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wne 2990
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 210  df-ne 2991
This theorem is referenced by:  pm2.61dane  3077  wefrc  5517  wereu2  5520  oe0lem  8125  fisupg  8754  marypha1lem  8885  fiinfg  8951  wdomtr  9027  unxpwdom2  9040  fpwwe2lem13  10057  grur1a  10234  grutsk  10237  fimaxre2  11578  xlesubadd  12648  cshwidxmod  14160  sqreu  14715  pcxcl  16190  pcmpt  16221  symggen  18593  isabvd  19587  lspprat  19921  mdetralt  21216  ordtrest2lem  21811  ordthauslem  21991  comppfsc  22140  fbssint  22446  fclscf  22633  tgptsmscld  22759  ovoliunnul  24114  itg11  24298  i1fadd  24302  fta1g  24771  plydiveu  24897  fta1  24907  mulcxp  25279  cxpsqrt  25297  ostth3  26225  brbtwn2  26702  colinearalg  26707  clwwisshclwws  27803  ordtrest2NEWlem  31273  subfacp1lem5  32539  frpomin  33186  frmin  33192  btwnexch2  33592  fnemeet2  33823  fnejoin2  33825  limsucncmpi  33901  areacirc  35143  sstotbnd2  35205  ssbnd  35219  prdsbnd2  35226  rrncmslem  35263  atnlt  36602  atlelt  36727  llnnlt  36812  lplnnlt  36854  lvolnltN  36907  pmapglb2N  37060  pmapglb2xN  37061  paddasslem14  37122  cdleme27a  37656  iccpartigtl  43927
  Copyright terms: Public domain W3C validator