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 3029
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 2947 . . 3 𝐴𝐵𝐴 = 𝐵)
3 pm2.61dne.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
42, 3syl5bi 232 . 2 (𝜑 → (¬ 𝐴𝐵𝜓))
51, 4pm2.61d 171 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1631  wne 2943
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 2944
This theorem is referenced by:  pm2.61dane  3030  wefrc  5243  wereu2  5246  oe0lem  7747  fisupg  8364  marypha1lem  8495  fiinfg  8561  wdomtr  8636  unxpwdom2  8649  fpwwe2lem13  9666  grur1a  9843  grutsk  9846  fimaxre2  11171  xlesubadd  12298  cshwidxmod  13758  sqreu  14308  pcxcl  15772  pcmpt  15803  symggen  18097  isabvd  19030  lspprat  19368  mdetralt  20632  ordtrest2lem  21228  ordthauslem  21408  comppfsc  21556  fbssint  21862  fclscf  22049  tgptsmscld  22174  ovoliunnul  23495  itg11  23678  i1fadd  23682  fta1g  24147  plydiveu  24273  fta1  24283  mulcxp  24652  cxpsqrt  24670  ostth3  25548  brbtwn2  26006  colinearalg  26011  clwwisshclwws  27165  ordtrest2NEWlem  30308  subfacp1lem5  31504  frpomin  32075  frmin  32079  btwnexch2  32467  fnemeet2  32699  fnejoin2  32701  limsucncmpi  32781  areacirc  33837  sstotbnd2  33905  ssbnd  33919  prdsbnd2  33926  rrncmslem  33963  atnlt  35122  atlelt  35246  llnnlt  35331  lplnnlt  35373  lvolnltN  35426  pmapglb2N  35579  pmapglb2xN  35580  paddasslem14  35641  cdleme27a  36176  iccpartigtl  41887
  Copyright terms: Public domain W3C validator