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 3028
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.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
21com12 32 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
3 pm2.61dne.2 . . 3 (𝜑 → (𝐴𝐵𝜓))
43com12 32 . 2 (𝐴𝐵 → (𝜑𝜓))
52, 4pm2.61ine 3025 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wne 2940
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 207  df-ne 2941
This theorem is referenced by:  pm2.61dane  3029  wefrc  5679  wereu2  5682  frpomin  6361  oe0lem  8551  fisupg  9324  marypha1lem  9473  fiinfg  9539  wdomtr  9615  unxpwdom2  9628  frmin  9789  fpwwe2lem12  10682  grur1a  10859  grutsk  10862  fimaxre2  12213  xlesubadd  13305  cshwidxmod  14841  sqreu  15399  pcxnn0cl  16898  pcxcl  16899  pcmpt  16930  symggen  19488  isabvd  20813  lspprat  21155  mdetralt  22614  ordtrest2lem  23211  ordthauslem  23391  comppfsc  23540  fbssint  23846  fclscf  24033  tgptsmscld  24159  ovoliunnul  25542  itg11  25726  i1fadd  25730  fta1g  26209  plydiveu  26340  fta1  26350  mulcxp  26727  cxpsqrt  26745  ostth3  27682  madebdaylemlrcut  27937  brbtwn2  28920  colinearalg  28925  clwwisshclwws  30034  ordtrest2NEWlem  33921  subfacp1lem5  35189  btwnexch2  36024  fnemeet2  36368  fnejoin2  36370  limsucncmpi  36446  areacirc  37720  sstotbnd2  37781  ssbnd  37795  prdsbnd2  37802  rrncmslem  37839  atnlt  39314  atlelt  39440  llnnlt  39525  lplnnlt  39567  lvolnltN  39620  pmapglb2N  39773  pmapglb2xN  39774  paddasslem14  39835  cdleme27a  40369  sdomne0  43426  sdomne0d  43427  modelaxreplem1  44995  iccpartigtl  47410
  Copyright terms: Public domain W3C validator