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 3018
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 3015 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1534  wne 2930
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 206  df-ne 2931
This theorem is referenced by:  pm2.61dane  3019  wefrc  5668  wereu2  5671  frpomin  6345  oe0lem  8535  fisupg  9318  marypha1lem  9469  fiinfg  9535  wdomtr  9611  unxpwdom2  9624  frmin  9785  fpwwe2lem12  10676  grur1a  10853  grutsk  10856  fimaxre2  12205  xlesubadd  13290  cshwidxmod  14806  sqreu  15360  pcxnn0cl  16857  pcxcl  16858  pcmpt  16889  symggen  19464  isabvd  20787  lspprat  21130  mdetralt  22598  ordtrest2lem  23195  ordthauslem  23375  comppfsc  23524  fbssint  23830  fclscf  24017  tgptsmscld  24143  ovoliunnul  25524  itg11  25708  i1fadd  25712  fta1g  26194  plydiveu  26323  fta1  26333  mulcxp  26709  cxpsqrt  26727  ostth3  27664  madebdaylemlrcut  27919  brbtwn2  28836  colinearalg  28841  clwwisshclwws  29945  ordtrest2NEWlem  33750  subfacp1lem5  35025  btwnexch2  35860  fnemeet2  36092  fnejoin2  36094  limsucncmpi  36170  areacirc  37427  sstotbnd2  37488  ssbnd  37502  prdsbnd2  37509  rrncmslem  37546  atnlt  39024  atlelt  39150  llnnlt  39235  lplnnlt  39277  lvolnltN  39330  pmapglb2N  39483  pmapglb2xN  39484  paddasslem14  39545  cdleme27a  40079  sdomne0  43117  sdomne0d  43118  iccpartigtl  47031
  Copyright terms: Public domain W3C validator