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 2909
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 2827 . . 3 𝐴𝐵𝐴 = 𝐵)
3 pm2.61dne.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
42, 3syl5bi 232 . 2 (𝜑 → (¬ 𝐴𝐵𝜓))
51, 4pm2.61d 170 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  pm2.61dane  2910  wefrc  5137  wereu2  5140  oe0lem  7638  fisupg  8249  marypha1lem  8380  fiinfg  8446  wdomtr  8521  unxpwdom2  8534  fpwwe2lem13  9502  grur1a  9679  grutsk  9682  fimaxre2  11007  xlesubadd  12131  cshwidxmod  13595  sqreu  14144  pcxcl  15612  pcmpt  15643  symggen  17936  isabvd  18868  lspprat  19201  mdetralt  20462  ordtrest2lem  21055  ordthauslem  21235  comppfsc  21383  fbssint  21689  fclscf  21876  tgptsmscld  22001  ovoliunnul  23321  itg11  23503  i1fadd  23507  fta1g  23972  plydiveu  24098  fta1  24108  mulcxp  24476  cxpsqrt  24494  ostth3  25372  brbtwn2  25830  colinearalg  25835  clwwisshclwws  26972  ordtrest2NEWlem  30096  subfacp1lem5  31292  frpomin  31863  frmin  31867  btwnexch2  32255  fnemeet2  32487  fnejoin2  32489  limsucncmpi  32569  areacirc  33635  sstotbnd2  33703  ssbnd  33717  prdsbnd2  33724  rrncmslem  33761  atnlt  34918  atlelt  35042  llnnlt  35127  lplnnlt  35169  lvolnltN  35222  pmapglb2N  35375  pmapglb2xN  35376  paddasslem14  35437  cdleme27a  35972  iccpartigtl  41684
  Copyright terms: Public domain W3C validator