Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61dne Structured version   Visualization version   GIF version

Theorem pm2.61dne 2868
 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 2786 . . 3 𝐴𝐵𝐴 = 𝐵)
3 pm2.61dne.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
42, 3syl5bi 231 . 2 (𝜑 → (¬ 𝐴𝐵𝜓))
51, 4pm2.61d 169 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780 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 196  df-ne 2782 This theorem is referenced by:  pm2.61dane  2869  wefrc  5032  wereu2  5035  oe0lem  7480  fisupg  8093  marypha1lem  8222  fiinfg  8288  wdomtr  8363  unxpwdom2  8376  fpwwe2lem13  9343  grur1a  9520  grutsk  9523  fimaxre2  10848  xlesubadd  11965  cshwidxmod  13400  sqreu  13948  pcxcl  15403  pcmpt  15434  symggen  17713  isabvd  18643  lspprat  18974  mdetralt  20233  ordtrest2lem  20817  ordthauslem  20997  comppfsc  21145  fbssint  21452  fclscf  21639  tgptsmscld  21764  ovoliunnul  23082  itg11  23264  i1fadd  23268  fta1g  23731  plydiveu  23857  fta1  23867  mulcxp  24231  cxpsqrt  24249  ostth3  25127  brbtwn2  25585  colinearalg  25590  clwwisshclww  26335  ordtrest2NEWlem  29296  subfacp1lem5  30420  frmin  30983  btwnexch2  31300  fnemeet2  31532  fnejoin2  31534  limsucncmpi  31614  areacirc  32675  sstotbnd2  32743  ssbnd  32757  prdsbnd2  32764  rrncmslem  32801  atnlt  33618  atlelt  33742  llnnlt  33827  lplnnlt  33869  lvolnltN  33922  pmapglb2N  34075  pmapglb2xN  34076  paddasslem14  34137  cdleme27a  34673  iccpartigtl  39961  clwwisshclwws  41235
 Copyright terms: Public domain W3C validator